Formal definition of the transformers from goto-program instructions to abstract event graphs (p. 10)

---

(1) assignment:  lhs=rhs; i
τ[lhs=rhs; i](aeg) = τ[i](( aeg.Es∪evts(lhs)∪evts(rhs), aeg.pos∪end(aeg.pos)×(evts(rhs)∪ evts(lhs)\trg(lhs))∪ (evts(rhs)∪evts(lhs)\trg(lhs)) ×trg(lhs), aeg.cmp ))
(2) function call:  fun(); i
τ[fun(); i] = τ[i] ∘ τ[body(fun)]
(3) guard:  [expr] i1; i2
τ[[guard] i1; i2] (aeg) = let guarded=τ[i1](aeg) in τ[i2] ((aeg.Es∪ guarded.Es, aeg.pos∪guarded.pos,aeg.cmp))
(4) forward jump:   goto l;
τ[goto l; i] = τ[follow(l)]
(5) backward jump:  l: i1; [cond] goto l; i2
τ[l: i1; [cond]goto l; i2] (aeg) = let local=τ[i1] (aeg) in τ[i2]((aeg.Es∪local.Es, aeg.pos∪ local.pos ∪ end(local.pos)× begin(local.pos),aeg.cmp))
(6) assume / assert / skip:   assume(φ); i / assert(φ); i / skip; i
τ[assume(φ); i] = τ[i]
(7) new thread:  start_thread th; i
τ [start_thread th; i](aeg) = let local=τ[body(th)](∅) and main=τ[i](aeg) and inter=τ[i](∅) in (local.Es∪main.Es, local.pos∪main.pos, local.Es⊗inter.Es)
(8) end of thread / function:  end_thread;
τ[end_thread](aeg) = aeg
(9) atomic section:  atomic_begin; i1; atomic_end; i2
τ[atomic_start; i1; atomic_end; i2](aeg) = let section=τ[i1]((aeg.Es,aeg.pos∪ end(aeg.pos)×{f}, aeg.cmp)) in τ[i2]((section.Es, section.pos∪ end(section.pos)×{f}, section.cmp))

Figure 1: Operations to create the aeg of a goto-program.

---

Notations: In Fig. 1, we use ⊗ to construct the cmp edges. We define ⊗ as A⊗ B={(x,y)|(x,y)∈ A× B s.t. write(x) ∨ write(y)}. We recall that evts(exp) is the set of abstract events derived from the shared variables accessed in expression exp. begin(S) and end(S) are respectively the sets of the first and last abstract events of the po_s sub-graph S. body(fun) designates the body of the function represented by the symbol fun. follow(l) represents the code following the label l in the code. f stands for a full fence and ∅ is a shortening for the triplet (∅,∅,∅).

This document was translated from L^AT_EX by H^EV^EA.