1. Declarative/Axiomatic Concurrency Semantics

• Define the notion of a program execution (generalization of an execution trace)
• Map a program to a set of executions
• Define a consistency predicate on executions
• Semantics = set of consistent executions of a program

<aside> 💡 Exception: “catch-fire” semantics → C/C++

Existence of at least one “bad” consistent execution implies undefined behavior.

• bad → data race </aside>

2. Executions

• Events
  • Reads, Writes, Updates, Fences
• Relations
  • Program order, po (also called “sequenced-before”, sb)
  • Reads-from, rf

<aside> 💡 Event

An event is a triple $\langle id, i, l \rangle$ where

• id ∈ N is an event identifier,
• i ∈ Tid ∪ {0} is a thread identifier, and
  • 0 is the default value
• l is a label.

Label

A label has one of of the following forms:

$$ Rx~v_r,~Wx~v_w,~U(x~v_r~v_w),~F $$

where $x ∈ Loc$ and $v_r , v_w ∈ Val$.

</aside>

<aside> 💡 Execution Graph

An execution graph is a tuple 〈 E, po, rf 〉 where:

• E is a finite set of events
• po (“program order”) is a partial order on E
• rf (“reads-from”) is a binary relation on E such that:
  • For every〈w, r〉 ∈ rf
    • typ(w) ∈ {W, U}
    • typ(r) ∈ {R, U}
    • loc(w) = loc(r)
    • $val_w (w) = val_r (r)$
  • $rf^{ −1}$ is a function (if 〈 w1, r 〉 , 〈 w2, r 〉 ∈ rf then w1 = w2 )
• Notations </aside>

3. Mapping Programs to Executions

Definition

The thread subsystem associates a sequential execution graph to every command.