arXiv:0910.5833v1 [] 30 Oct 2009

From Single-thread to Multithreaded: An
E ient Stati Analysis Algorithm
Jean-Loup Carré

Charles Hymans

November 2, 2009

Abstra t
A great variety of stati analyses that ompute safety properties of
single-thread programs have now been developed. This paper presents
a systemati method to extend a lass of su h stati analyses, so that
they handle programs with multiple POSIX-style threads. Starting
from a pragmati operational semanti s, we build a denotational semanti s that expresses reasoning à la assume-guarantee. The nal
algorithm is then derived by abstra t interpretation. It analyses ea h
thread in turn, propagating interferen es between threads, in addition
to other semanti information. The ombinatorial explosion, ensued
from the expli it onsideration of all interleavings, is thus avoided.
The worst ase omplexity is only in reased by a fa tor n ompared
to the single-thread ase, where n is the number of instru tions in the
program. We have implemented prototype tools, demonstrating the
pra ti ality of the approa h.

1

Introdu tion

Many stati

analyses have been developed to

he k safety properties of se-

quential programs [1, 2, 3, 4, 5℄ while more and more software appli ations
are multithreaded. Naive approa hes to analyze su h appli ations would run
by exploring all possible interleavings, whi h is impra ti al. Some previous
proposals avoid this

ombinatorial explosion (see Related Work). Our

tribution is to show that

every

stati

on-

analysis framework for single-thread

programs extends to one that analyzes multithreaded

1

ode with dynami

1

INTRODUCTION

thread

2

reation and with only a modest in rease in

on urren y spe i

bugs, e.g., ra e

authors [6℄. If any, su h bugs

omplexity. We ignore

onditions or deadlo ks, as do some other

an be dete ted using orthogonal te hniques

[7, 8℄.

Outline

We des ribe in Se tion 2 a toy imperative language.

This

tains essential features of C with POSIX threads [9℄ with a thread
primitive. The main feature of multithreaded
may

interfere,

on-

reation

ode is that parallel threads

i.e., side-ee ts of one thread may

hange the value of vari-

ables in other threads. To take interferen e between threads into a

ount,

we model the behavior of a program by an innite transition system: this is
the operational semanti s of our language, whi h we des ribe in Se tion 2.3.
It is

ommon pra ti e in abstra t interpretation to go from the

the abstra t semanti s through an intermediate so- alled
ti s [10℄. In our

G-

ase a dierent but similar

on ept is needed, whi h we

olle ting semanti s, and whi h we introdu e in Se tion 3.

ti s will dis over states, a
thread and

on rete to

olle ting semanThis seman-

umulate transitions en ountered in the

olle t interferen es from other threads.

urrent

The main properties

of this semanti sProposition 2 and Theorem 1are the te hni al
this paper.

all

These properties allow us to overapproximate the

G-

ore of

olle ting

semanti s by a denotational semanti s. Se tion 4 then derives an abstra t
semanti s from the

G-

olle ting semanti s through abstra t interpretation.

We dis uss algorithmi

issues, implementation, question of pre ision, and

possible extensions in Se tion 5, and examine the
te hnique in se tion 6, and

Related Work

omplexity of our analysis

on lude in Se tion 7.

A great variety of stati

analyses that

ompute safety

properties of single-thread programs have been developed, e.g., intervals [4℄,
points-to-graph [11, 3℄, non-relational stores [1, 2℄ or relational stores su h
as o tagons [5℄.
Our approa h is similat to Rugina and Rinard [12, 13℄, in the sens that
we also use an abstra t semanti s that derives tuples
about

urrent states, transitions of the

other threads.

ontaining information

urrent thread, and interferen e from

While their main parallel primitive is

threads ans waits for their

ompletion before resuming

mostly interested in the more
whi h spawn a thread that

hallenging thread

par ,

whi h runs too

omputation, we are

reation primitive

create ,

an survive its father. In Se tion 6.3, we handle

2

SYNTAX AND OPERATIONAL SEMANTICS

par

to show how they

3

an be dealt with our te hniques.

Some authors present generalizations of spe i

analyses to multithreaded

ode, e.g., Venet and Brat [14℄ and Lammi h and Müller-Olm [6℄, while our
framework extends any single-threaded

ode analysis.

Our approa h also has some similarities with Flanagan and Qadeer [15℄.
They use a model- he king approa h to verify multi-threaded programs.
Their algorithm
see our stati

omputes a guarantee

analysis framework as

ondition for ea h thread; one

an

omputing a guarantee, too. Further-

more, both analyses abstra t away both number and ordering of interferen es
from other threads. Flanagan and Qadeer's approa h still keeps some
rete information, in the form of triples

ontaining a thread id, and

on-

on rete

stores before and after transitions.

They

polynomial time in the size of the

omputed set of triples. However, su h

sets

laim that their algorithm takes

an have exponential size in the number of global variables of the pro-

gram. When the nesting depth of loops and thread

reation statements is

bounded, our algorithm works in polynomial time.

Moreover, we demon-

strate that our analysis is still pre ise on realisti

examples. Finally, while

Flanagan and Qadeer assume a given, stati , set of threads
gram start-up, we handle dynami
required in Malkis

et al. [16℄.

thread

reated at pro-

reation. The same restri tion is

The 3VMC tool [17℄ has a more general s ope. This is an extension of
TVLA designed to do shape analysis and to dete t spe i

multithreaded

bugs. However, even without multithreading, TVLA already runs in doubly
exponential time [18℄.
Other papers fo us on bugs that arise be ause of multithreading primitives. This is orthogonal to our work. See [19, 20℄ for atomi ity properties,
Lo ksimth and Goblint tools [7, 21, 22℄ for data-ra es and [8℄ for deadlo k
dete tion using geometri

2

ideas.

Syntax and Operational Semanti s

2.1 Simplied Language.
The syntax of our language is given in Fig. 1. The syntax of the language
is de omposed in two parts:
ommands (cmd ) and statements (stmt ). A
′
statement cmd , ℓ is a ommand with a return label where it should go after
ℓ
ℓ
ompletion. E.g., in Fig 2a, a thread at label ℓ3 will exe ute 3 create( 4 x :=

2

SYNTAX AND OPERATIONAL SEMANTICS

4

lv

::=
left value
cmd ::=
ommand
| x
variable
ℓ
| lv := e
assignment
| ∗e
pointer deref
| cmd 1 ; cmd 2
sequen e
e
::=
expression
| if (cond )then{cmd 1 }else{cmd 2 } if
| c
onstant
| ℓ while(cond){cmd}
while
| lv
left value
| ℓ create(cmd )
new thread
| o(e1 , e2 ) operator
stmt ::=
statement
| &x
address
′
| cmd , ℓ
ommand
cond ::=
ondition
| ℓ guard(cond), ℓ′
guard
| x
variable
ℓ
′′
′
| spawn(ℓ ), ℓ
new thread
| ¬cond negation
Figure 1: Syntax

ℓ1

x := 0;
ℓ2
while(true)
{ℓ3 create(ℓ4 x := x + 1)}, ℓ∞
(a) ℓ1 example 1 , ℓ∞
ℓ1

y := 0; ℓ2 z := 0;
ℓ3
create(ℓ4 y := y + z);
ℓ5
z := 3, ℓ∞
( ) ℓ1 example 3 , ℓ∞

ℓ5

x := 0; ℓ6 y := 0;
ℓ7
create(ℓ8 x = x + y);
ℓ9
y := 3, ℓ∞
(b) ℓ5 example 2 , ℓ∞

ℓ10

y := 0; ℓ11 z := 0;
ℓ12
create(ℓ13 y := 3);
ℓ14
y := 1; ℓ15 z := y, ℓ∞
(d) ℓ10 example 4 , ℓ∞
Figure 2: Program Examples

x + 1), ℓ2 .

Commands and statements are labeled, and we denote by

Labels

ℓ
′
ontrol ow: the statement stmt, ℓ
′
and terminates at label ℓ , e.g., in Fig 2b, a thread at label ℓ2

the set of labels. Labels represent the
begins at label

ℓ

will exe ute the assignment
a given

x := x+1 and go to label ℓ3 .

It is assumed that in

ommand or statement ea h label appears only on e. Furthermore, to

represent the end of the exe ution, we assume a spe ial label
appears in a

ℓ∞

whi h never

ommand, but may appear as the return label of a statement.

Intuitively, this label represents the termination of a thread: a thread in this
label will not be able to exe ute any statement.
Noti e that sequen es

cmd 1 ; cmd 2

are not labeled. Indeed, the label of

a sequen e is impli itly the label of the rst

ommand, e.g., the program of

2

SYNTAX AND OPERATIONAL SEMANTICS

5

ℓ
Fig. 2b is a sequen e labeled by ℓ5 . We write cmd when the label of cmd is
ℓ
′
ℓ and we write stmt, ℓ the statement stmt labeled by ℓ and ℓ′ . A program is
ℓ
represented by a statement of the form cmd , ℓ∞ . Other statements represent
a partial exe ution of a program. The statements
atomi , there are

create , while

and

if

are not

steps, e.g., to enter in a while
ℓ
steps, we introdu e the statements 1 spawn(ℓ2 ), ℓ3

omposed of several basi

loop. To model these basi
ℓ
and 1 guard(cond ), ℓ2 . Then, the semanti s of create , while and if will be
ℓ
ℓ
dened using the semanti s of 1 spawn(ℓ2 ), ℓ3 and 1 guard(cond ), ℓ2 . Lo al
variables are irrelevant to our work. Then, all variables in our language are
global. Nevertheless, lo al variables have been implemented (See Se tion 5)
as a sta k.
This is a toy imperative language with dynami

thread

reation. It

an

easily be extended to handle real-world languages like C or Ada, see Se tions
2.4 and 5.

2.2 Des ription of the system.
To represent threads, we use a set

Ids

of

thread identiers.

During an exe-

ution of a program, ea h thread is represented by a dierent identier. We
assume a distinguished identier

main ∈ Ids,

and take it to denote the

initial thread.
When a program is exe uted, threads go from a label to another one
independently.

A

ontrol point

is a partial fun tion

identiers to labels and that is dened in
ea h thread with its

urrent label.

main .

A

The domain of

P

that maps thread

ontrol point asso iates

P

is the set of

reated

threads, the other identiers may be used after in the exe ution, for new

P be the set of ontrol points. We write Dom(P ) the domain
def
let P [i 7→ ℓ] be the partial fun tion dened by P [i 7→ ℓ](j) =
if i = j
if i ∈ Dom(P ) r {j}

threads. Let

 P and

ℓ
P (j)



of

undened

else

Furthermore, threads may

reate other threads at any time. A

genealogy

(i, ℓ, j) ∈ Ids×Labels×Ids su h that
(i2 , ℓ2 , j2 ) have distin t third omponent

of threads is a nite sequen e of tuples
(a) ea h two tuples

(i.e.,
tuple
been

(i1 , ℓ1 , j1 )

and

j1 6= j2 ), (b) main is never the third omponent of a tuple. Su h a
(i, ℓ, j) means that thread i reated thread j at label ℓ. We write j has
reated in g to say that a uple (i, ℓ, j) appears in g . Let Genealogies

2

SYNTAX AND OPERATIONAL SEMANTICS

6

on atenation

′
of the genealogies
be the set of genealogies. We write g · g the
′
g and g . The hypothesis (a) means that a thread is never reated twi e,
the hypothesis (b) means that the thread

main

is never

reated: it already

exists at the begining of the exe ution.
We let

Stores

be the set of

stores.

We leave the pre ise semanti s of

stores undened for now, and only require two primitives

write lv:=e (σ)

and

bool (σ, cond). Given a store σ , write lv:=e returns the store modied by the
assignment lv := e. The fun tion bool evaluates a ondition cond in a store
σ , returning true or false .
A uple (i, P, σ, g) ∈ Ids × P × Stores × Genealogies is a state if (a) i ∈
Dom(P ), (b) Dom(P ) is the disjoint union between {main } and the set of
threads reated in g . Let States be the set of states. A state is a tuple
(i, P, σ, g) where i is the urrently running thread, P states where we are
in the ontrol ow, σ is the urrent store and g is the genealogy of thread
reations. Dom(P ) is the set of existing threads. The hypothesis (a) means
that the

urrent thread exists, the hypothesis (b) means that the only threads

that exist are the initial threads and the thread
In the single-threaded

reated in the past.

ase, only the store and the

unique thread is needed. In the
ea h thread is needed: this is

ontrol point of the

ase of several threads, the

ontrol point of

P.

There are two standard ways to model interferen es between threads:

•

Either all threads are a tive, and at any time any threads

an re a

transition,

•

or, in ea h state there is an a tive thread, a.k.a., a  urrent thread,
and some so

alled s hedule transitions

Our model rests on latter
during exe ution.

an

hange the a tive thread.

hoi e: this allows us to keep tra k of a thread

Thread ids do not

arry information as to how threads

reated. This is the role of the g omponent of states.
ℓ
Given a program 0 cmd , ℓ∞ the set Init of initial states is the set of

were

(main , P0 , σ, ǫ) where Dom(P0 ) = {main }, P0 (main ) = ℓ0 , σ is an
ǫ is the empty word.

′
′
′
′
A transition is a pair of states τ = (i, P, σ, g), (i , P , σ , g · g ) su h that
∀j ∈ Dom(P ) r {i}, P (j) = P ′ (j) and if (j, ℓ, j ′ ) is a letter of g ′, then j = i
and P (i) = ℓ.
def
We denote by Tr the set of all transitions and we denote by Schedule =
{((i, P, σ, g), (j, P, σ, g)) ∈ Tr | i 6= j} the set of transitions that may appear
tuples

arbitrary store, and

2

SYNTAX AND OPERATIONAL SEMANTICS

7

σ ′ = write lv:=e (σ)
bool(σ, cond ) = true
assign ℓ
guard
ℓ1
′
1
lv := e, ℓ2 ⊢ (ℓ1 , σ) → (ℓ2 , σ )
guard(cond ), ℓ2 ⊢ (ℓ1 , σ) → (ℓ2 , σ)
ℓ1
ℓ1
guard(cond), ℓ2 ⊢ t
guard(¬cond ), ℓ3 ⊢ t
while
entry
while exit
ℓ1
ℓ2
ℓ1
while(cond ){ cmd }, ℓ3 ⊢ t
while(cond){ℓ2 cmd}, ℓ3 ⊢ t
ℓ1
guard(cond), ℓ2 ⊢ t
then
ℓ1
if (cond)then{ℓ2 cmd 1 }else{ℓ3 cmd2 }, ℓ4 ⊢ t
ℓ1
guard(¬cond ), ℓ3 ⊢ t
else
ℓ1
if (cond)then{ℓ2 cmd 1 }else{ℓ3 cmd2 }, ℓ4 ⊢ t
ℓ1
P (i) = ℓ
stmt, ℓ2 ⊢ (ℓ, σ) → (ℓ′ , σ ′ )
parallel
ℓ1
stmt, ℓ2 (i, P, σ, g) → (i, P [i 7→ ℓ′ ], σ ′ , g)
P (i) = ℓ1
j is fresh in (i, P, σ, g)
P ′ = P [i 7→ ℓ3 ][j 7→ ℓ2 ]
spawn
ℓ1
spawn(ℓ2 ), ℓ3 (i, P, σ, g) → (i, P ′ , σ, h · (i, ℓ2 , j))
ℓ2
cmd , ℓ4 τ
then body
ℓ1
ℓ3
if (cond )then{ cmd 2 }else{ℓ3 cmd2 }, ℓ4 τ
ℓ2
cmd , ℓ4 τ
else body
ℓ1
ℓ2
if (cond )then{ cmd 1 }else{ℓ3 cmd2 }, ℓ4 τ
ℓ1
ℓ2
spawn(ℓ2 ), ℓ3 τ
cmd, ℓ1 τ
while body
reate
ℓ1
ℓ2
ℓ1
create( cmd ), ℓ3 τ
while(cond ){ℓ2 cmd }, ℓ3 τ
ℓ1
ℓ2
cmd 1 , ℓ2 τ
cmd 2 , ℓ3 τ
sequen
e
1
sequen e 2
ℓ1
ℓ2
ℓ1
cmd 1 ; cmd 2 , ℓ3 τ
cmd 1 ; ℓ2 cmd 2 , ℓ3 τ
ℓ2
P (j) is dened
i 6= j
cmd , ℓ∞ τ
hild
s hedule
ℓ1
ℓ2
ℓ
′
create( cmd ), ℓ3 τ
stmt, ℓ
(i, P, σ, g) → (j, P, σ, g)
Figure 3: Operational semanti s rules

in the
only

on lusion of rule s hedule, respe tively.

hanges the identier of the

A transition in

Schedule

urrent thread.

2.3 Evolution.
To model interleavings, we use a small step semanti s: ea h statement gives
rise to an innite transition system over states where edges
spond to elementary
ℓ
judgment 1 stmt, ℓ2

s1 → s2

orre-

s1 to s2 . We dene the
s1 → s2 is one of these global
′
exe uted, returning to label ℓ

omputation steps from state

s1 → s2

to state that

omputation steps that arise when

cmd

on termination. To simplify semanti

is

rules, we use an auxiliary judgment

2

SYNTAX AND OPERATIONAL SEMANTICS

ℓ1

stmt, ℓ2 ⊢ (ℓ, σ) → (ℓ′ , σ ′ )

8

to des ribe evolutions that are lo al to a given

thread.
Judgments are derived using the rules of Fig. 3. The rule parallel transforms lo al transitions into global transitions. While body and sequen e
rules are global be ause while loop and sequen es may ontain global subℓ
ℓ
ℓ
ommands, e.g., 1 while(x){ 2 create( 3 x := 0)}. In spawn, the expression
 j is fresh in

(i, P, σ, g) means that i 6= j and P (j) is not dened and j
g , i.e., in g , there is no tuples (i, ℓ, i′ ) with i or i′ equal to

nevers appears in

j.

Intuitively, a fresh identier is an identier that has never been used (we

keep tra k of used identiers in

g ).

We dene the set of transitions generated by the statement

Tr ℓ stmt,ℓ′ = {(s, s′ ) | ℓ stmt, ℓ′

ℓ

stmt, ℓ′ :

s → s′ }.

Noti e that, unlike Flanagan and Qadeer [15℄, an arbitrary number of
threads may be spawned, e.g., with the program
Therefore,

Ids is innite, an so are P and Tr ℓ stmt,ℓ′ .

ℓ1 example 1 , ℓ∞ of Fig. 2a.
Furthermore, Stores may

be innite, e.g., if store maps variables to integers. Therefore, we
a

omplexity depending of

Example

Let us

ardinal of

annot have

Tr ℓ stmt,ℓ′ .

onsider stores that are maps from a unique variable to

an integer. We write

[x = n]

the store that maps

x

to the integer

n.

The

transitions generated by the statements extra ted from Fig. 2a are:

Tr ℓ1 x:=0,ℓ2 ={((i, P, [x = n], g), (i, P [i 7→ ℓ2 ], [x = 0], g)) | P (i) = ℓ1
∧ i ∈ Ids ∧ n ∈ Z}.
Tr ℓ4 x:=x+1,ℓ∞ ={((i, P, [x = n], g), (i, P [i 7→ ℓ∞ ], [x = n + 1], g)) | P (i) = ℓ4
∧ i ∈ Ids ∧ n ∈ Z}.

2.4 Properties of the language
Let

Labs(ℓ cmd , ℓ∞ )

be the set of labels of the statement

ℓ

cmd , ℓ∞ .

We also dene by indu tion on ommands, the set of labels of subthreads
Labs child (·) by Labs child (ℓ1 create(ℓ2 cmd ), ℓ3 ) = Labs(ℓ2 cmd , ℓ∞ ),
Labs child (ℓ1 cmd 1 , ℓ2 cmd 2 , ℓ3 ) = Labs child (ℓ1 cmd 1 , ℓ2 ) ∪ Labs child (ℓ2 cmd 2 , ℓ3 ),
Labs child (ℓ1 if (cond)then{ℓ2 cmd 1 }else{ℓ3 cmd 2 }, ℓ4 ) =
Labs child (ℓ2 cmd 1 , ℓ4 ) ∪ Labs child (ℓ3 cmd 2 , ℓ4 ),

3

G-COLLECTING SEMANTICS

9

Labs child (ℓ1 while(cond ){ℓ2 cmd }, ℓ3) = Labs child (ℓ2 cmd 1 , ℓ1 ),
ℓ
and, for basi
ommands Labs child ( 1 basic, ℓ2 ) = ∅.
A statement generates only transitions from its labels and to its labels,
this is formalized by the following lemma:

Lemma 1. If (s, s′ ) ∈ Tr ℓ stmt,ℓ′ r Schedule then label (s) ∈ Labs(ℓ stmt, ℓ′ ) r

{ℓ′ } and label(s′ ) ∈ Labs(ℓ stmt, ℓ′ ) and thread (s) = thread (s′ ).
As a

onsequen e of Lemma 1, we have the following lemma :

Lemma 2. If label(s) ∈/ Labs(ℓ stmt, ℓ′ ) r {ℓ′ } then for all state s′ , (s, s′ ) ∈/
Tr ℓ stmt,ℓ′ r Schedule
If, during the exe ution of a statement

ℓ

stmt, ℓ′ ,

thred, then, the subthread is in a label of the
Labs child (ℓ stmt, ℓ′ ).

a thread

reates another

ommand, furthermore, it is in

Lemma 3. If (s, s′ ) = ((i, P, σ, g), (i′, P ′ , σ′ , g ′)) ∈ Tr ℓ stmt,ℓ′ r Schedule and

j ∈ Dom(P ′ ) r Dom(P ) then P ′(j) ∈ Labs child (ℓ stmt, ℓ′ ) ⊆ Labs(ℓ stmt, ℓ′ ).

Lemma 4. If (s, s′ ) ∈ Tr ℓ stmt,ℓ′ rSchedule and label (s) ∈ Labs child (ℓ stmt, ℓ′ )r
{ℓ′ } then label (s′ ) ∈ Labs(ℓ stmt, ℓ′ ).
Furthermore ℓ ∈
/ Labs(ℓ stmt, ℓ′ ) and ℓ′ ∈
/ Labs(ℓ stmt, ℓ′ ).

Noti e that in Fig. 3 some statements are atomi . We

basi statements.

ments
ℓ
form 1 lv

:=

On basi

all these state-

Formally, a basi statement is a statement of the
ℓ1
e, ℓ2 , guard(cond ), ℓ2 or ℓ1 spawn(ℓ3 ), ℓ2 .
statement, we have a more pre ise lemma on labels:

Lemma 5. Let ℓ1 basic, ℓ2 be a basi statement.

If (s, s′ ) = ((i, P, σ, g), (i′, P ′ , σ ′ , g ′)) ∈ Tr ℓ1 basic,ℓ2 r Schedule then thread (s) =
thread (s′ ) and label (s) = ℓ1 and label (s′ ) = ℓ2 .

3

G-

olle ting Semanti s

3.1 Basi Con epts
To prepare the grounds for abstra tion, we introdu e an intermediate semanti s,

alled

G-

olle ting semanti s, whi h asso iates a fun tion on

tions with ea h statement.

ongura-

The aim of this semanti s is to asso iate with

3

G-COLLECTING SEMANTICS

10

def

thread (i, P, σ, g) = i
def
label (i, P, σ, g) = P (i)
def
after (i, P, σ, g) = {(j, P ′ , σ ′ , g · g ′ ) ∈ States|j ∈ desc g′ ({i})}
For X ⊆ P(Ids) :
def

• desc ǫ (X) = X
•

and

(
desc g (X ∪ {j})
desc (i,ℓ,j)·g (X) =
desc g (X)

if

def

i∈X

else

Figure 4: Auxiliary denitions

ea h statement a transfer fun tion that will be abstra ted (see Se tion 4) as
an abstra t transfer fun tion.
A

on rete onguration

of the system during an exe ution,
urrent thread and its des endants
what the other threads

Q = hS, G, Ai : 1. S is the urrent state
2. G, for guarantee, represents what the
an do 3. and A, for assume, represents

is a tuple

an do.

Formally, S is a set of states, and G and A are sets of transitions ontaining
Schedule . The set of on rete ongurations is a omplete latti e for the
ordering hS1 , G1 , A1 i 6 hS2 , G2 , A2 i ⇔ S1 ⊆ S2 ∧ G1 ⊆ G2 ∧ A1 ⊆ A2 . Proposition
4 will establish the link between operational and G- olle ting semanti s.
Figure 5 illustrates the exe ution of a whole pro-

j1

gram. Ea h verti al line represents the exe ution of a
thread from top to bottom, and ea h horizontal line
represents the

reation of a thread. At the beginning

(top of the gure), there is only the thread

j3

j0

•s0

main = j0 .

j2

•s
j5

During exe ution, ea h thread may exe ute transitions. At state

running thread
Fig. 5, the
thread of

s

s0 , thread (s0 )

urrent thread of
is

denotes the

urrent thread ),

(or

s0

is

j0

ates

j1
j3 .

is a

j6

urrently

see Fig. 4.
and the

On

Figure 5: States

urrent

j2 .
j0

During the program exe ution given in Fig. 5,
that

j4

hild

of

j0

and

j0

is the

We then introdu e the

a des endant of

j0

parent

on ept of

be ause it has been

of

j1 .

reates

Furthermore,

des endant :

reated by

j1

j1 .

We say

j1

the thread

whi h has been

re-

j3

is
re-

3

G-COLLECTING SEMANTICS

11

j0 . More pre isely, des endants depend on genealogies. Consider
the state s0 = (j0 , P0 , σ0 , g0 ) with g0 = [(j0 , ℓ1 , j1 )]: the set of des endants
of j0 from g0 (written desc g0 ({j0 }), see Fig. 4) is just {j0 , j1 }. The set of

ated by

des endants of a given thread in reases during the exe ution of the pro-

s is of the form g0 · g for some g , here
g = [(j0 , ℓ2 , j2 ), (j1 , ℓ3 , j3 ), (j2 , ℓ4 , j4 )]. When the exe ution of the program
rea hes the state s, the set of des endants of j0 from g0 · g is desc g0 ·g ({j0 }) =
{j0 , j1 , j2 , j3 , j4 }.

gram.

In Fig. 5, the genealogy of

In a genealogy, there are two important pie es of information. First, there
is a tree stru ture: a thread

reates

hildren that may

reates

g,

j2

on... Se ond, there is a global time, e.g., in
before the thread

the thread

hildren and so

has been

reated

j3 .

Lemma 6. Let g · g ′ a genealogy and i, j whi h are not reated in g ′ . Therefore, either desc g′ ({j}) ⊆ desc g·g′ ({i}) or desc g′ ({j}) ∩ desc g·g′ ({i}) = ∅.

Proof.

We prove this lemma by indu tion on

g ′.

If

g ′ = ǫ,

then

desc ǫ ({j}) =

{j}.
g ′ = g ′′ · (i′ , ℓ, j ′ ). By indu tion hypothesis either
desc g′′ ({j}) ⊆ desc g·g′′ ({i}) or desc g′′ ({j}) ∩ desc g·g′′ ({i}) = ∅.
′
′
In the rst ase, if i ∈ desc g ′′ ({j}), therefore j ∈ desc g ′′ ·(i′ ,ℓ′ ,j ′ ) ({j}) and
′
′
j ∈ desc g·g′′ ·(i′ ,ℓ′ ,j ′ ) ({i}), else j ∈
/ desc g′′ ·(i′ ,ℓ′ ,j ′ ) ({j}).
′
In the se ond ase, let us onsider the sub ase i ∈ desc g ′′ ({j}). Therefore
i′ ∈
/ desc g·g′′ ({i}). In addition to this, j is not reated in g · g ′′ (a thread
annot be reated twi e in a genealogy), therefore j ∈
/ desc g·g′′ ({i}). Hen e
′
′
j ∈ desc g′′ ·(i′ ,ℓ′ ,j ′) ({j}) and j ∈
/ desc g·g′′ ·(i′ ,ℓ′ ,j ′) ({i}).
′
′′
The sub ase i ∈ desc g·g ({i}) is similar. Let us onsider the sub ase
i′ ∈
/ desc g′′ ({j})∪desc g·g′′ ({i}). Therefore desc g·g′′ ·(i′ ,ℓ′ ,j ′) ({i}) = desc g·g′′ ({i})
and desc g ′′ ·(i′ ,ℓ′ ,j ′ ) ({j}) = desc g ′′ ({j}).
Let us

onsider the

ase

g . In this partial genealdesc g ({j0 }) = {j0 , j2 , j4 }. Noti e
even though the reation of j3 is in the genealogy g .
During an exe ution, after having en ountered a state s0 = (j0 , P0 , σ0 , g0 )
we distinguish two kinds of des endants of j0 : (i) those whi h already exist in
state s0 (ex ept j0 itself ) and their des endants, (ii) j0 and its other des enWe also need to

onsider sub-genealogies su h as

j1 has not been
that j3 ∈
/ desc g ({j0 })
ogy,

reated by

j0 .

Hen e

dants. Ea h thread of kind (i) has been

j0 .

We

all

after (s0 ) the states from whi

reated by a statement exe uted by
h a thread of kind (ii)

an exe ute a

3

G-COLLECTING SEMANTICS

12

transition. In Fig. 5, the thi k lines des ribe all the states en ountered while
exe uting the program that fall into

after (s0 ).

The following lemma expli its some properties of

after :

Lemma 7. Let T a set of transitions. Let (s0 , s1 ) ∈ T ⋆ therefore:
1. If thread (s0 ) = thread (s1 ) then s1 ∈ after(s0 )
2. If s1 ∈ after (s0 ) then after(s1 ) ⊆ after (s0 )
Proof.

(i0 , P0 , σ0 , g0 ) = s0 and (i1 , P1 , σ1 , g1 ) = s1 . By denition of
g1′ su h that g1 = g0 · g1′ . Be ause i0 ∈ desc ǫ ({i0 }),
i0 ∈ desc g1′ ({i0 }). Therefore, if thread (s) = thread (s′ ), i.e., i1 = i0 , then
s1 ∈ after (s0 ) (By denition of after ).
Let us assume that s1 ∈ after (s0 ). Let s2 = (i2 , P2 , σ2 , g2 ) ∈ after(s1 ).
′
′
′
′
Therefore, there exists g2 su h that g2 = g1 · g2 = g0 · g1 · g2 and i2 ∈
desc g2′ ({i1 }). Be ause s1 ∈ after(s0 ), by denition, i1 ∈ desc g1′ ({i0 }). Therefore i1 ∈ desc g ′ ({i1 })∩desc g ′ ·g ′ ({i0 }). A ording to Lemma 6, desc g ′ ({i1 }) ⊆
2
1 2
2
desc g1′ ·g2′ ({i0 }). Hen e i2 ∈ desc g1′ ·g2′ ({i0 }) and therefore s2 ∈ after(s0 ).
Let

transitions, there exists

When a s hedule transition is exe uted, the
futur des endants of the past

urrent thread

urrent thread and the new

hange. The

urrent thread are

dients. This is formalized by the following lemma:

Lemma 8. If (s1 , s2 ) ∈ Schedule then after (s1 ) ∩ after(s2 ) = ∅.
Proof.

(i1 , P1 , σ1 , g1 ) = s1 and i2 = thread (s2 ). Therefore (i2 , P1 , σ1 , g1 ) =
s = (i, P, σ, g) ∈ after (s1 ) ∩ after(s2 ).
′
′
By denition of after , there exists g su h that g = g1 · g , i ∈ desc g ′ ({i1 })
and i ∈ desc g ′ ({i2 }). Furthermore i1 and i2 are in Dom(P1 ). Therefore i1 and
i2 are either reated in g1 , or are main . Hen e, i1 and i2 annot be reated
′
in g . Therefore, i2 ∈
/ desc g′ ({i1 }) and therefore desc g′ ({i2 }) ⊆ desc ǫ·g′ ({i1 }).
Using Lemma 6 we on lude that desc g ′ ({i1 }) ∩ desc g ′ ({i2 }) = ∅. This is a
ontradi tion with i ∈ desc g ′ ({i1 }) and i ∈ desc g ′ ({i2 }).
s2 .

Let

Let

During the exe ution of a set of transition

T

that do not

reate threads,

the set of des endants does not in rease:

Lemma 9. Let T a set of transitions su h that:
for all (s, s′ ) = ((i, P, σ, g), (i′, P ′, σ ′ , g ′)) ∈ T, g = g ′.
Let s0 = (i0 , P0 , σ0 , g0 ), s = (i, P, σ, g0 · g) and s = (i′ , P ′ , σ ′ , g0 · g · g ′).
If (s, s′ ) ∈ (A|after (s0 ) ∪ T )⋆ then desc g·g′ {i0 } = desc g {i0 }.

3

G-COLLECTING SEMANTICS

Proof.

13

s1 , . . . , sn a sequen e of states su h that s1 = s, for all k ∈
{1, . . . , n − 1}, (sk , sk+1) ∈ A|after (s0 ) ∪ T )⋆ , and sn = s′ .
Let (ik , Pk , σk , g0 · g · gk ) = sk .
If gk 6= gk+1 then, (sk , sk1 ) ∈ A|after (s ) and then ik ∈
/ desc g·gk {i0 } and then
0
desc g·gk {i} = desc g·gk+1 {i0 }.
Therefore, in all ases desc g·gk {i} = desc g·gk+1 {i} and then, by straightforward indu tion, desc g·g ′ {i} = desc g {i}.
Let

Lemma 10. Let T a set of transitions su h that:

for all (s, s′ ) = ((i, P, σ, g), (i′, P ′, σ ′ , g ′)) ∈ T, g = g ′.
Let s = (i, P, σ, g) and s = (i′ , P ′, σ ′ , g · g ′ ).
If (s, s′ ) ∈ (A|after (s0 ) ∪ T )⋆ then desc g′ {i} = {i}.
Proof.

Apply Lemma 9 with

These lemmas has a

s0 = s.

onsequen e on

after :

Lemma 11. Let T a set of transitions su h that:

for all (s, s′ ) = ((i, P, σ, g), (i′, P ′, σ ′ , g ′)) ∈ T, g = g ′.
If (s0 , s1 ) ∈ (A|after (s0 ) ∪ T )⋆ and s1 ∈ after (s0 ) then thread (s1 ) = thread (s0 ).
Proof.

Let (i0 , P0 , σ0 , g0 ) = s0 and (i1 , P1 , σ, g0 · g1 ) = s1 .
desc g1 {i0 } = {i0 } and by denition of after , i1 ∈ desc g1 {i0 }.

By Lemma 10

Lemma 12. Let T1 a set of transitions su h that:
for all (s, s′ ) = ((i, P, σ, g), (i′, P ′, σ ′ , g ′)) ∈ T, g = g ′.
Let T2 a set of transitions.
Let s0 , s1 , s three states su h that (s0 , s1 ) ∈ T1⋆ , thread (s0 ) = thread (s1 )
and (s1 , s) ∈ T ⋆ .
If s ∈ after (s0 ) then s ∈ after (s1 ).
Proof.

(i0 , P0 , σ0 , g0 ) = s0 , (i1 , P1 , σ, g0 ·g1) = s1 and (i, P, σ, g0 ·g1 ·g) = s.
desc g1 {i0 } = {i0 } and by denition of after , i1 ∈ desc g1 {i0 }.
Therefore desc g1 ·g ({i0 }) = desc g (desc g1 ({i0 })) = desc g ({i0 }).
Be ause s ∈ after (s0 ), idesc g1 ·g ({i0 }), therefore idesc g ({i0 }). Hen e s ∈
after (s1 ).
Let

By Lemma 10

3

G-COLLECTING SEMANTICS

j0

j1

•s0

j0

j1

•s0

j3

•s1 j
5

(a) Reach

j0

j1

•s0

j2

j3

•s1 j
5

(b) Reach

•s1 j
5
( ) Par

Figure 6:

14

G-

j4

j0

•s0

j3

j2

•s1 j
5

j4
j6

(d) Sub

olle ting semanti s

3.2 Denition of the G- olle ting Semanti s
Let us re all some lassi al denitions. For any binary relation R on states
′
let R|S = {(s, s ) ∈ R | s ∈ S} be the
of R to S and RhSi =
′
′
′
′′
{s | ∃s ∈ S : (s, s ) ∈ R} be the
of R on S . R; R = {(s, s ) |
′
′
′
′ ′′
′
∃s ∈ States
: (s, s ) ∈ R ∧ (s , s ) ∈ R } is the
of R and R . Let
S
⋆
0
k+1
k
R = k∈N R where R = {(s, s) | s ∈ States} and R
= R; Rk . Finally,

restri tion
appli ation
omposition

omplement

S , let S = States r S be the
 of S.
ℓ
The denition of the G- olle ting semanti s
stmt, ℓ′ of a statement
ℓ
stmt, ℓ′ requires some intermediate relations and sets. The formal denition
for any set of states

is given by the following denition:

Denition 1.
ℓ

where:


def
stmt, ℓ′ hS, G, Ai = hS′ , G ∪ Self ∪ Par ∪ Sub, A ∪ Par ∪ Subi
ℓ
def
stmt, ℓ′ hS, G, Ai = [Reach, Ext, Self, Par, Sub]

Reach =




⋆ 
(s0 , s1 ) ∈ (G|after (s0 ) ∩ Tr ℓ stmt,ℓ′ ) ∪ A|after(s0 )
(s0 , s1 )
∧thread (s0 ) = thread (s1 ) ∧ label(s0 ) = ℓ

S′ = {s1 |s1 ∈ ReachhSi ∧ label (s1 ) = ℓ′ }
Self = {(s, s′ ) ∈ Tr ℓ stmt,ℓ′ |s ∈ ReachhSi}
Par = {(s, s′ ) ∈ Tr ℓ stmt,ℓ′ |∃s0 ∈ S : (s0 , s) ∈ Reach; Schedule ∧ s ∈ after (s0 )}
⋆

Ext(s0 , s1 ) = (G|after(s0 ) ∩ Tr ℓ stmt ,ℓ′ ) ∪ A|after (s0 ) ∪ G|after (s1 )


∃s0 , s1 ∈ S × S′ : (s0 , s1 ) ∈ Reach∧
′
Sub = (s, s )
(s1 , s) ∈ Ext(s0 , s1 ) ∧ s ∈ after (s0 ) r after (s1 )

3

G-COLLECTING SEMANTICS

15

Let us read together, on some spe ial

ases shown in Fig. 6. This will

explain the rather intimidating of Denition 1 step by step, introdu ing the
ne essary

ompli ations as they

ome along.

s0 = (j0 , P, σ, g)

The statement is exe uted between states

s1 =

and

(j0 , P ′, σ ′ , g · g ′).
Figure 6(a) des ribes the single-thread ase: there is no thread intera tion
ℓ
′
during the exe ution of stmt, ℓ . The thread j5 is spawned after the exe ution
ℓ
of the statement. E.g., in Fig. 2b, 6 y := 0; ℓ7 .
In this simple
exists a path from

ase, a state

s0

to

s

s

is rea hable from

s0

if and only if there

using only transitions done by the unique thread

(these transitions should be in the guarantee G) and that are generated by
′
the statement. S represents the nal states rea hable from S. Finally, in this
ase:


⋆
Reach = {(s0 , s1 ) ∈ G ∩ Tr ℓ stmt ,ℓ′ |label (s0 ) = ℓ}
S′ = {s1 | s1 ∈ Reach(S) ∧ label(s1 ) = ℓ′ }
Self = {(s, s′ ) ∈ Tr ℓ stmt,ℓ′ | s ∈ Reach(S)}
ℓ

stmt, ℓ′ hS, G, Schedulei = hS′ , G ∪ Self, ScheduleiPar

Figure 6(b) is more

omplex:

j0 interferes with
A. Some states

interferen es are assumed to be in

= Sub = ∅

threads

j1

and

su h interferen e transitions. E.g,

y, ℓ∞ in Fig. 2d:
the statement
label

ℓ15 .

j3 .

These

an be rea hed only with
ℓ
ℓ
onsider the statement 14 y := 1; 15 z :=

at the end of this statement, the value of z may be
ℓ13
y := 3, ℓ∞ may be exe uted when the thread

3, be

main

ause
is at

Therefore, to avoid missing some rea hable states, transitions of

A

are taken into a ount in the denition of Reach. In Fig. 6(b), the statement
ℓ
stmt, ℓ′ is exe uted by des endants of j0 of kind (ii) (i.e., after (s0 )), and the
interferen es

after (s0 )).

ome from

j1

and

Finally, we nd the

Reach =



j3

whi h are des endants of kind (i) (i.e., in

omplete formula of Denition 1:

⋆ 

(s0 , s1 ) ∈ (G|after (s0 ) ∩ Tr ℓ stmt,ℓ′ ) ∪ A|after (s0 )
.
(s0 , s1 )
∧thread (s0 ) = thread (s1 ) ∧ label(s0 ) = ℓ

In Fig. 6( ), when j0 exe utes the statement
(j2 and

j4 )

antee

is not supposed to

G

ℓ

stmt, ℓ′ it

reates subthreads

whi h exe ute transitions in parallel of the statement. The guarontain only transitions exe uted by the

urrent

thread but also these transitions. These transitions, represented by thi k lines
in Fig. 6( ), are

olle ted into the set

Par.

Consider su h a transition, it is ex-

e uted in parallel of the statement, i.e., from a state of

Schedule◦Reach({s0 }).

3

G-COLLECTING SEMANTICS

(s, s′ ) ∈ (A|after (s) ∪ Schedule)⋆
s ∃s ∈ S :
∧thread (s) = thread (s′ )


′ ∃s = (i, P, σ, g · (i, ℓ, j)) ∈ States :
s
s′ ∈ after(s)


(i, P, σ, g ′) ∈ S
′
(j, P, σ, g ) ∃i, g :
∧g ′ = g · (i, ℓ, j)
hinterfereA∪(G|post (ℓ) ) ◦ s hedule- hild (S),
Schedule, A ∪ (G|post(ℓ) )i
hinterfereA∪G′ (S), G ∪ G′ , A ∪ G′ i
G′ with hS′ , G′ , A′ i = f hS, G, Ai
exe ute-thread↑ω
f,S,A (G)


def

interfereA (S) =

def

post(ℓ) =

def

s hedule- hild(S) =

def

init- hildℓ (hS, G, Ai) =

def

ombinehS,G,Ai (G′ ) =
def
exe ute-threadf,S,A (G) =
def
guaranteef hS, G, Ai =

′

Figure 7: Basi

Furthermore, this transition
lier thread, hen e from

16

semanti



fun tions

ame from the statement, and not from an ear-

after (s0 ).

Par = {(s, s′) ∈ Tr ℓ stmt,ℓ′ | ∃s0 ∈ S : (s0 , s) ∈ Schedule◦Reach∧s ∈ after(s0 )}.
The threads

reated by

j0

when it exe utes the statement

survive when this statement returns in
thread

i (here, i

is

j4

or

j5

or

j6 )

s1 ,

ℓ

stmt, ℓ′

as shown in Fig. 6(d).

Su h a

an exe ute transitions that are not in

i

may

Par.

create statement
′
exe uted between s0 and s1 . Hen e, su h a transition (s, s ) is exe uted
from a state in after(s0 ) r after (s1 ). The path from s1 to s is omprised
of transitions in (G|after(s0 ) ∩ Tr ℓ stmt,ℓ′ ) ∪ A|after (s ) (similarly to Reach) and of
0
transitions of j0 or j5 under the dotted line, i.e., transitions in G|after (s1 ) .
Sub

olle ts these transitions. The

reation of

results of a

3.3 Properties of the G- olle ting Semanti s
To prepare for our stati

G-

analysis we provide a

ompositional analysis of the

olle ting semanti s in Theorem 1 below. To this end, we introdu e a set

of helper fun tions, see Fig. 7.
def S
f ↑ω (X) = n∈N f n (X).
1A

We dene, for any extensive

1

fun tion

f,

fun tion f of domain D is extensive if and only if for every set X ⊆ D, X ⊆ f (X)

3

G-COLLECTING SEMANTICS

17

interfereA (S) returns states that are rea hable
applying interferen es in A. Noti e that these interferen es do not
The fun tion

label of the

from

S

by

hange the

urrent thread:

Lemma 13. Let s = (i, P, σ, g) and s′ = (i′ , P ′, σ′ , g ′). If (s, s′) ∈ (A|after (s) ∪
Schedule)⋆ then P (i) = P ′ (i), i.e., label (s) = P ′(thread (s)).
If furthermore thread (s) = thread (s′ ) then label (s) = label(s′ ).

Proof.

s0 , . . . , sn su h that s0 = s and
sn = s and for all k ∈ {0, . . . , n − 1}, (sk , sk+1 ) ∈ A|after(s) ∪ Schedule .
Let (ik , Pk , σk , gk ) = sk . Let us prove by indu tion that Pk (i) = P (i). If
(sk , sk+1 ) ∈ Schedule and Pk (i) = P (i) then Pk+1(i) = P (i). If (sk , sk+1 ) ∈
A|after (s) and Pk (i) = P (i) then sk ∈
/ after (sk ) and then ik 6= i and then
Pk+1 (i) = Pk (i) = P (i).
There exists a sequen e of states

′

The fun tion
after having

post(ℓ)

transition to the last
omputes a

omputes the set of states that may be rea hed

reated a thread at label
hild of the

onguration for the last

genealogies to dene

post(ℓ)

applies a s hedule

urrent thread. The fun tion

interferen es with its parent using

exe ute-thread

ℓ; s hedule- hild
hild

reated at

post(ℓ);

ℓ,

init- hildℓ

taking into a

ount

noti e that we need here the

and then to have Theorem 1.

The fun tion

omputes a part of the guarantee (an under-approximation),

f from onguraexe ute-thread to ompute

given the semanti s of a ommand represented as a fun tion
tion to

onguration. And

guarantee

iterates

the whole guarantee.
During the exe ution of a statement

ℓ

stmt, ℓ′ , some interferen

e transition

may be red at any time. Nevertheless, the labels of the thread(s) exe uting
the statement are still in a label of the statement:

Lemma 14. If (s0 , s) ∈ (Tr ℓ stmt,ℓ′ ∪ A|after (s0) )∗ , label (s0 ) ∈ Labs(ℓ stmt, ℓ′ )

and s ∈ after(s0 ) then label (s) ∈ Labs(ℓ stmt, ℓ′ ).
Futhermore, if label (s) = ℓ′ or label (s) = ℓ then thread (s0 ) = thread (s).

Proof. There exists a path s1 , . . . , sn su h that sn = s and for all k ∈
{0, . . . , n − 1}, (sk , sk−1) ∈ Tr ℓ stmt,ℓ′ ∪ A|after (s0 ) . Let (i0 , P0 , σ0 , g0 ) = s0 and
for k > 1, let (ik , Pk , σk , g0 · gk ) = sk .
ℓ
′
Let us prove by indu tion on k that Pk (i) ∈ Labs( stmt, ℓ ) and for all
ℓ
′
j ∈ desc gk ({i0 }) r {i0 }, Pk (j) ∈ Labs child ( stmt, ℓ ).
Let us assume that k satisfy the indu tion property, and let us show that
k + 1 saties the indu tion property.

3

G-COLLECTING SEMANTICS

18

(sk , sk+1) ∈ A|after(s0 ) , ik ∈
/ desc gk ({i0 }) and then for all j =
desc gk ({i0 }) = desc gk+1 ({i0 }), Pk (j) = Pk+1 (j).
In the ase (sk , sk+1 ) ∈ Tr ℓ stmt,ℓ′ and ik = i0 , by Lemma 1, Pk+1 (ik ) ∈
Labs(ℓ stmt, ℓ′ ). Furthermore, if j ∈ desc gk ({i0 }) then Pk (j) = Pk+1 (j). If
j ∈ desc gk+1 ({i0 }) r desc gk ({i0 }), then j ∈ Dom(Pk+1 ) r Dom(Pk ) and by
ℓ
′
Lemma 3, Pk+1 (j) ∈ Labs child ( stmt, ℓ ).
In the ase(sk , sk+1 ) ∈ Tr ℓ stmt,ℓ′ and ik = i0 , we on lude similarly by
Lemma 4. If s ∈ after (s0 ), then in ∈ desc gn ({i0 }) and therefore label (s) ∈
Labs(ℓ stmt, ℓ′ ).
′
′
If label (s) = ℓ or label(s) = ℓ, then, be ause by Lemma 4, ℓ and ℓ are
ℓ
′
not in Labs child ( stmt, ℓ ), we have thread (s0 ) = thread (s).
In the

ase

The following lemma summarizes the

onsequen es on

Reach

of Lemmas

7 and 14:

Lemma 15. Let [Reach, Ext, Self, Par, Sub] =

stmt, ℓ′ hS, G, Ai.
If (s0 , s) ∈ Reach therefore s ∈ after (s0 ), after(s) ⊆ after (s0 ) and
label(s) ∈ Labs(ℓ stmt, ℓ′ ).

⋆
Proof. (s0 , s) ∈ (G|after (s0 ) ∩ Tr ℓ stmt,ℓ′ ) ∪ A|after (s0 ) , then by Lemma 7, s ∈
after (s0 ) and after (s) ⊆ after (s0 ). Furthermore, by Lemma 14, label(s) ∈
Labs(ℓ stmt, ℓ′ ).
The following proposition show that

ℓ

guarantee

olle t all transitions

generated by a statement.

Proposition 1 (Soundness of guarantee ). Let hS, G, Ai a on rete onguration, ℓ stmt, ℓ′ a statement and G∞ = guarantee ℓ stmt,ℓ′  hS, G, Ai. Let s0 ∈ S

and s ∈ after(s0 ) su h that (s, s′ ) ∈ Tr ℓ stmt,ℓ′ .
⋆
If (s0 , s) ∈ (Tr ℓ stmt,ℓ′ )|after(s0 ) ∪ A|after (s0 ) then (s, s′) ∈ G∞
Proof.

 G
hSk , Gk , Ak i = exe ute-threadk ℓ
stmt,ℓ′ ,S,A
ℓ

and [Reachk , Extk , Selfk , Park , Subk ] =
stmt, ℓ′ hS, Gk , Ai
and T = Tr ℓ stmt,ℓ′
′
Let s0 , . . . , sn+1 a path su h that sn = s, sn+1 = s and for all k ,

⋆
(sk , sk+1 ) ∈ T|after (s0 ) ∪ A|after (s0 ) . Let m an arbitrary integer. Then, let k0
the smallest k (if it exists) su h that (sk , sk+1 ) ∈ T|after (s0 ) r Gm . Then, by
denition, (sk , sk+1 ) ∈ Selfm ∪ Parm ⊆ Gm+1 ⊆ G∞ .
Let

3

G-COLLECTING SEMANTICS

19

3.4 Basi Statements
Basi

statement have

ommon properties, therefore, we will study them at

the same time. Proposition 2 explain how to overapproximate the semanti s
of a basi

statement. It will be used in the abstra t semanti s.

An exe ution path of a basi

statement

feren es, then one transition of the basi

an be de omposed in inter-

statement, and then, some other

interferen es. The following lemma show this. This lemma will allow us to
prove Proposition 2.

Lemma 16. Let ℓ1 basic, ℓ2 be a basi
 statement,

and [Reach, Ext, Self, Par, Sub] =
then:

ℓ1

basic, ℓ2 hS, G, Ai. Let (s0 , s) ∈ Reach

• either s ∈ interfereA ({s0 }) and label(s) = ℓ1 ,
• or s ∈ interfereA (Tr ℓ1 basic,ℓ2 r SchedulehinterfereA ({s0 })i)
and label (s) = ℓ2

Proof.

(s0 , s) ∈ (A|after (s0 ) ∪Schedule)⋆ . By denition
of Reach, thread (s0 ) = thread (s). Therefore s ∈ interfere A ({s0 }). By
Lemma 13, label (s0 ) = label (s), hen e, label (s) = ℓ1 .
Let us onsider the ase (s0 , s) ∈
/ (A|after(s0 ) ∪ Schedule)⋆ Be ause (s0 , s) ∈
Reach, (s0 , s) ∈ [(G|after (s0 ) ∩ Tr ℓ1 basic,ℓ2 )A|after (s0 ) ]⋆ . So (s0 , s) ∈ (A|after (s0 ) ∪
Schedule)⋆ ; [G|after(s0 ) ∩Tr ℓ1 basic,ℓ2 rSchedule]; [(G|after (s0 ) ∩Tr ℓ1 basic,ℓ2 )A|after (s0 ) ]⋆ .
Let s1 , s2 , s3 , . . . , sn a sequen e of states su h that (s1 , s2 ) ∈ (A|after (s ) ∪
0
Schedule)⋆ and (s2 , s3 ) ∈ G|after (s0 ) ∩ Tr ℓ1 basic,ℓ2 r Schedule and for all k ∈
{3, . . . , n}, (sk , sk+1 ) ∈ (G|after (s0 ) ∩ Tr ℓ1 basic,ℓ2 )A|after (s0 ) .
Noti e that (s1 , s2 ) ∈ G|after (s0 ) and therefore s1 ∈ after (s0 ). By Lemma
11, thread (s0 ) = thread (s1 ). Therefore s1 ∈ interfere A ({s0 }).
By Lemma 5, label(s2 ) = ℓ2 .
Let k0 the smallest (if it exists) k > 2 su h that (sk , sk+1 ) ∈ Tr ℓ1 basic,ℓ2 r
Schedule . Therefore (s2 , sk0 ) ∈ (A|after (s0 ) ∪ Schedule)⋆ . By Lemma 13,
label(sk0 ) = label(s2 ) = ℓ2 . A ording to Lemma 5, this is a ontradi tion.
Therefore, for all k ∈ {3, . . . , n}, (sk , sk+1 ) ∈ Schedule ∪ A|after(s ) .
0
By Lemma 1, thread (s1 ) = thread (s2 ), hen e thread (s2 ) = thread (s).
Therefore s2 ∈ interfere A ({s2 })
Let us

onsider the

ase

Now, we introdu e some

laims on the semanti s of basi

Claims 1 and 2 say that when a basi

statements.

statement is exe uted, only one thread

3

G-COLLECTING SEMANTICS

is exe uted. Noti e that
The Claim 3

spawn

20

reates a subthread, but does not exe ute it.

ara terizes the transitions done by the urrent thread. The
S′ , the set of states rea hed at the

Claim 4 gives an overapproximation of
end of the exe ution of a basi

statement.

Claim 1. Let ℓ1 basic, ℓ2 a basi statement and [Reach, Ext, Self, Par, Sub] =

ℓ1
basic, ℓ2 hS, G, Ai. Therefore, Par = ∅.
Proof.

(s, s′ ) ∈ Par. Therefore, (s, s′ ) ∈ Reach; SchedulehSi. So, there
exists s0 ∈ S0 and s1 su h that (s0 , s1 ) ∈ Reach, (s1 , s) ∈ Schedule and
s ∈ after (s0 ). Hen e, by Lemma 7, thread (s) = thread (s′ ). Given that
(s, s1 ) ∈ Reach, thread (s) = thread (s1 ). But, be ause (s1 , s) ∈ Schedule ,
thread (s) 6= thread (s1 ). There is a ontradi tion. Hen e Par = ∅.
Let

Claim 2. Let ℓ1 basic, ℓ2 a basi statement and [Reach, Ext, Self, Par, Sub] =

ℓ1
basic, ℓ2 hS, G, Ai. Therefore, Sub = ∅.
Proof.

(s, s′ ) ∈ Sub. There exists s0 ∈ S and s1 su h that (s0 , s1 ) ∈
Reach, (s2 , s) ∈ Ext(s0 , s1 ) and s ∈ after (s0 ) r after (s1 ).
Let (i0 , P0 , σ0 , g0 ) = s0 and (i1 , P1 , σ1 , g0 · g1 ) = s1 . Be ause (s0 , s1 ) ∈
Reach, thread (s0 ) = thread (s1 ). Let j ∈ desc g1 ({i0 }). Let s′1 = (j, P1 , σ1 , g0 ·
g1 ). Therefore s′1 ∈ after(s0 ) and (s0 , s′1 ) ∈ (Tr ℓ1 basic,ℓ2 ∪A|after (s0 ) )⋆ ; (Schedule ⋆ ).
′
By lemma 11, j = thread (s1 ) = thread (s0 ) = i0 . Hen e desc g1 ({i0 }) = {i0 }.
Let (i, P, σ, g0 · g1 · g) = s. By denition of desc and a straightforward
indu tion on g , desc g1 ·g ({i0 }) = desc g ({i0 }).
Be ause s ∈ after (s0 ), then i ∈ desc g1 ·g ({i0 }). Therefore i = i0 . By
Lemma 7, s ∈ after (s1 ). This is ontradi tory with s ∈ after (s0 ) r after(s1 ).
Hen e Sub = ∅.
Let

Claim 3. Let ℓ1 basic, ℓ2 a basi statement and [Reach, Ext, Self, Par, Sub] =

ℓ1
basic, ℓ2 hS, G, Ai.
Therefore, Par ⊆ {(s, s′ ) ∈ Tr ℓ1 basic,ℓ2 | s ∈ interfereA (S)} ∪ Schedule .
Proof.

(s, s′ ) ∈ Self r Schedule . Then (s, s′ ) ∈ Tr ℓ1 basic,ℓ2 and s ∈
ReachhSi. Then, there exists s0 ∈ S su h that (s0 , s) ∈ Reach. Be ause
(s0 , s) ∈ Tr ℓ1 basic,ℓ2 r Schedule , by Lemma 5, label (s) = ℓ1 6= ℓ2 . By Lemma
16, s ∈ interfere A ({s0 }) ⊆ interfere A (S). Be ause thread (s0 ) = thread (s),
(s, s′ ) ∈ Self.

ℓ
′ ′ ′
1
hS, G, Ai
Claim 4. Let ℓ1 basic, ℓ2 a basi statement,
hS
,
G
,
A
i
=
basic,
ℓ
2
ℓ
1
and [Reach, Ext, Self, Par, Sub] =
basic, ℓ2 hS, G, Ai.

′
Therefore, S ⊆ interfereA Tr ℓ1 basic,ℓ2 r SchedulehinterfereA (S)i .
Let

3

G-COLLECTING SEMANTICS

Proof.

21

s ∈ S′ . Therefore, label (s) = ℓ2 and there exists s0 ∈ S su h that
(s0 , s) ∈ Reach.
Be ause label (s) = ℓ2 6= ℓ1 , a ording to Lemma 16, s ∈ interfere A (Tr ℓ1 basic,ℓ2 r
SchedulehinterfereA ({s0 })i) ⊆ interfere A (Tr ℓ1 basic,ℓ2 rSchedulehinterfereA (S)i)
Let

Proposition 2 (Basi

statements)

 ℓ1

. Let ℓ1 basic, ℓ2 be a basi statement, then:


basic, ℓ2 hS, G, Ai 6 hS′′ , G ∪ Gnew , Ai

where S′′ = interfereA Tr ℓ1 basic,ℓ2 r SchedulehinterfereA (S)i
and Gnew = {(s, s′ ) ∈ Tr ℓ1 basic,ℓ2 | s ∈ interfereA (S)}
Proof.

This proposition is a straightforward



onsequen e of Claims 1, 2, 3

and 4.

3.5 Overapproximation of the G- olle ting Semanti s
The next theorem shows how the

G-

olle ting semanti s an be over-approximated

by a denotational semanti s, and is the key point in dening the abstra t semanti s.

Theorem 1. 1.



 

cmd 1 ; ℓ2 cmd 2 , ℓ3 (Q) 6 ℓ2 cmd 2 , ℓ3 ◦ ℓ1 cmd 1 , ℓ2 (Q)


ℓ2
ℓ4
2.  ℓ1 if ((cond)then{
cmd
}else{
cmd
},
ℓ
(Q) 6  
1
2
3
 



ℓ2
cmd 1 , ℓ3 ◦ ℓ1 guard(cond ), ℓ2 (Q)⊔ ℓ4 cmd 2 , ℓ3 ◦ ℓ1 guard(¬cond ), ℓ4 (Q)


ℓ

1
},
ℓ
(Q)
6
guard(¬cond
),
ℓ
◦ loop↑ω (Q)
3. ℓ1 while(cond ){ℓ2 cmd
3
3





with loop(Q′ ) = ℓ2 cmd, ℓ1 ◦ ℓ1 guard(cond ), ℓ2 (Q′ ) ⊔ Q′


4. ℓ1 create(ℓ2 cmd ), ℓ3 (Q) 6 ombineQ′ ◦guarantee ℓ2 cmd,ℓ  ◦init- hildℓ2 (Q′ )
∞


with Q′ = ℓ1 spawn(ℓ2 ), ℓ3 (Q)
of

ℓ

1

While points 1 and 3 are as expe ted, the overapproximation of semanti s
ℓ1
create(ℓ2 cmd), ℓ3 (point 4) omputes interferen es whi h will arise from

exe uting the

hild and its des endants with

this result with the

onguration of the

guarantee

and then

ombines

urrent thread. This theorem will

be proved later.
The following proposition

T.

The only

onstraint on

T

onsider a statement
is on the use of labels

ℓ

stmt, ℓ′ set
ℓ
′
of stmt, ℓ .

of transition

3

G-COLLECTING SEMANTICS

The proposition

22

onsider an exe ution of the statement from a state

a state s1 , and, after, an exe ution
ℓ
′
of stmt, ℓ mays only be used :

s2 , . . . , sn

of other

•

for interferen es,

•

or by the statement,

•

after having applied the statement, i.e., after

s0

to

ommands. The labels

s1 .

. This Proposition ensures us that any transition exe uted by a thread reℓ
′
ated during the exe ution of stmt, ℓ (i.e., between s0 and s1 ) is a transition
ℓ
′
generated by the statement stmt, ℓ .

Proposition 3. Let ℓ stmt, ℓ′ astatement,

[Reach, Ext, Self, Par, Sub] = ℓ stmt, ℓ′ hS, G, Ai. Let (s0 , s1 ) ∈ Reach and
T a set of transitions su h that for all (s, s′ ) ∈ T , if label (s) ∈ Labs(ℓ stmt, ℓ′ )
then (s, s′ ) ∈ Tr ℓ stmt,ℓ′ or s ∈ after (s1 ) ∪ after (s0 ).
Let s2 , . . . , sn a sequen e of states su h that for all k ∈ {1, . . . , n − 1},
(sk , sk+1 ) ∈ T . Therefore, if sk ∈ after(s0 ) then either sk ∈ after (s1 ) or
(sk , sk+1 ) ∈ Tr ℓ stmt,ℓ′

Proof.

Let for all

k > 1,

let

(ik , Pk , σk , g0 · gk ) = sk .

Let us show by indu tion on k > 1 that for all j , if j ∈ desc g0 ·gk ({i1 }) r
desc gk ({i1 }) then Pk (j) ∈ Labs(ℓ stmt, ℓ′ ).
′
Let j0 ∈ desc g0 ·gk ({i1 }) r desc g0 ({i1 }) and s1 = (j0 , P1 , σ1 , g0 · g1 ). There′
′
fore s1 ∈ after (s0 ). Given that(s0 , s1 ) ∈ Reach; Schedule , by Lemma 15,
P1 (j1 ) = label (s′1 ) ∈ Labs(ℓ stmt, ℓ′ ).
By indu tion hypothesis, for all
ℓ
′
then Pk−1 (j) ∈ Labs( stmt, ℓ ).

j,

if

j ∈ desc g0 ·gk−1 ({i1 }) r desc gk−1 ({i1 })

j ∈ desc g0 ·gk ({i1 }) r desc gk ({i1 }).
thread (sk−1 ) = j , therefore, sk−1 ∈ after (s0 ) r after (s1 ). Furtherℓ
′
more, by indu tion hypothesis, Pk−1 (j) = label(sk−1 ) ∈ Labs( stmt, ℓ ). By
denition of T , (sk−1 , sk ) ∈ Tr ℓ stmt,ℓ′ . By Lemma 1, Pk (j) = label (sk ) ∈
Labs(ℓ stmt, ℓ′ ).
If j ∈ Dom(Pk ) r Dom(Pk−1 ), then, thread (sk−1 ) ∈ desc g0 ·gk−1 ({i1 }) r
desc gk−1 ({i1 }). Hen e, as above, (sk−1 , sk ) ∈ Tr ℓ stmt,ℓ′ . Hen e, a ording to
ℓ
′
Lemma 3, Pk (j) = label(sk ) ∈ Labs( stmt, ℓ ).
Else, by denition of a transition, Pk−1 (j) = Pk (j).
Let

If

3

G-COLLECTING SEMANTICS

23

k su h that sk ∈ after(s0 ), hen e, either sk ∈ after(s1 ), or sk ∈
/
after (s1 ). In the last ase ik ∈ desc g0 ·gk−1 ({i1 })rdesc gk−1 ({i1 }), and therefore
label(sk ) ∈ Labs(ℓ stmt, ℓ′ ). Hen e, by denition of T , (sk , sk+1 ) ∈ Tr ℓ stmt,ℓ′ .
Let

3.5.1 Proof of Property 1 of Theorem 1
Lemma 17. Tr ℓ1 cmd 1 ;ℓ2 cmd 2 ,ℓ3 = Tr ℓ1 cmd 1,ℓ2 ∪ Tr ℓ2 cmd 2 ,ℓ3
In this se tion, we onsider an initial onguration : Q0 = hS0 , G0 , A0 i and
ℓ
ℓ
a sequen e 1 cmd 1 ; 2 cmd 2 , ℓ3 . We write Tr 1 = Tr ℓ1 cmd 1 ,ℓ2 and Tr 2 = Tr ℓ2 cmd 2 ,ℓ3
and

′

Tr = Tr ℓ1 cmd 1 ;ℓ2 cmd 2 ,ℓ3

Dene:
′ ′



Q = hS , G , A′ i = ℓ1 cmd 1 ; ℓ2 cmd 2 , ℓ3 (Q0 )
ℓ1
K = [Reach, Ext, Self,
cmd 1 ; ℓ2 cmd 2 , ℓ3 (Q0 )
 =
 ℓ Par, Sub]
Q1 = hS1 , G1 , A1 i = 1 cmd 1 , ℓ2 (Q0 )

K1 = [Reach1 , Ext1 ,Self1 , Par1, Sub1 ] = ℓ1 cmd 1 , ℓ2 (Q0 )
Q2 = hS2 , G2 , A2 i = ℓ2 cmd 2 , ℓ3 (Q1 )

K2 = [Reach2 , Ext2 , Self2 , Par2 , Sub2 ] = ℓ2 cmd 2 , ℓ3 (Q1 )

Lemma 18. If (s, s′ ) ∈ Tr and label (s) ∈ Labs(ℓ1 cmd 1 , ℓ2 ) r {ℓ2 } then
(s, s′ ) ∈ Tr 1 .
If (s, s′ ) ∈ Tr and label (s) ∈ Labs(ℓ2 cmd 2 , ℓ3 ) then (s, s′ ) ∈ Tr 2 .

Proof.

ℓ
Let us onsider that label (s) ∈ Labs( 1 cmd 1 , ℓ2 )r{ℓ2 }. Hen e be ause
ℓ
ℓ
labels of 1 cmd1 ; 2 cmd 2 , ℓ3 are pairwise distin t, label(s) ∈
/ Labs(ℓ2 cmd 3 , ℓ3 ).
′
′
By Lemma 2, (s, s ) ∈
/ Tr 2 . Hen e, by Lemma 17, (s, s ) ∈
/ Tr 1
ℓ2
The ase label (s) ∈ Labs( cmd 2 , ℓ3 ) is similar.

Lemma 19. Using the above notations, for every (s0 , s) ∈ Reach su h that
s0 ∈ S0 ,

• either (s0 , s) ∈ Reach1 and label(s) 6= ℓ2
• or there exists s1 ∈ S1 su h that (s0 , s1 ) ∈ Reach1 , (s1 , s) ∈ Reach2

Proof.

(s0 , s) ∈ Reach1 or (s0 , s) ∈
/ Reach1 .
In the rst ase, either label (s) 6= ℓ2 , or label (s) = ℓ2 . If label(s) = ℓ2 ,
then, by denition, s ∈ S1 . By denition, (s, s) ∈ Reach2 and (s, s) ∈
Ext1 (s0 , s). We just have to hoose s1 = s.
Let

(s0 , s) ∈ Reach.

Either

3

G-COLLECTING SEMANTICS

24

/ Reach1 . Let T0 = (G0|after(s0 ) ∩Tr 1 )∪A0 |after(s0 ) .
In the se ond ase, (s0 , s) ∈
′
′
Sin e (s, s ) ∈ Reach , thread (s0 ) = thread (s) and label(s0 ) = ℓ1 . Furthermore (s0 , s) ∈
/ Reach1 , so (s0 , s) ∈
/ T0⋆ . Sin e (s, s′ ) ∈ Reach′ ⊆ [(G0|after (s0 ) ∩
Tr ) ∪ A0 |after (s0 ) ]⋆ , Tr = Tr 1 ∪ Tr 2 (using Lemma 17) and Tr 1 ⊃ Schedule ,
⋆
therefore (s0 , s) ∈ [T0 ∪ (G0|after(s0 ) ∩ Tr 2 r Schedule)] .
⋆
⋆
Re all (s0 , s) ∈
/ T , hen e (s0 , s) ∈ T0 ; (G0|after (s0 ) ∩ Tr 2 r Schedule); [T0 ∪
(G0|after (s0 ) ∩ Tr 2 )]⋆ . Therefore, there exists s1 , s2 su h that:
• (s0 , s1 ) ∈ T0⋆
• (s1 , s2 ) ∈ G0 |after (s0 ) ∩ Tr 2 r Schedule
• (s2 , s) ∈ [T0 ∪ (G0|after (s0 ) ∩ Tr 2 )]⋆
s0 ∈ S0 , label(s0 ) = ℓ1 ∈ Labs(ℓ1 cmd 1 , ℓ2 ). Sin e (s1 , s2 ) ∈ G0|after (s0 ) ,
s1 ∈ after (s0 ). Furthemore (s0 , s1 ) ∈ T0⋆ ⊆ Tr 1 ∪ A0 |after (s0 ) , so, a ording to
ℓ
Lemma 14, label (s1 ) ∈ Labs( 1 cmd 1 , ℓ2 ).
Given that (s1 , s2 ) ∈ Tr 2 r Schedule , a ording to Lemma 2, label(s1 ) ∈
Labs(ℓ2 cmd 2 , ℓ3 ). Hen e label (s1 ) ∈ Labs(ℓ2 cmd 2 , ℓ3 ) ∩ Labs(ℓ1 cmd 1 , ℓ2 ). Beℓ
ℓ
ause the labels of 1 cmd 1 ; 2 cmd 2 , ℓ3 are pairwise distin ts, label (s1 ) = ℓ2 .
Using Lemma 14, we on lude that thread (s0 ) = thread (s1 ).
⋆
Given that thread (s0 ) = thread (s) and label(s0 ) = ℓ1 and (s0 , s1 ) ∈ T0 ,
we on lude that (s0 , s1 ) ∈ Reach1 . Furthermore label (s1 ) = ℓ2 and s0 ∈ S0 ,
therefore s1 ∈ S1 .
(s1 , s) ∈ [T0 ∪ (G0|after(s0 ) ∩ Tr 2 )]⋆ . Therefore, by proposition 3, (s1 , s) ∈
[T0 ∪ (G0|after(s1 ) ∩ Tr 2 )]⋆ ⊆ Ext1 (s0 , s1 ).
⋆
Re all that (s2 , s) ∈ [T0 ∪ (G0|after (s0 ) ∩ Tr 2 )] , then there exists s3 , . . . , sn
su h that for all k ∈ {3, . . . , n − 1}, (sk , sk+1 ) ∈ T0 ∪ (G0 |after (s0 ) ∩ Tr 2 ). By
denition, if (sk , sk+1 ) ∈ G0|after (s0 ) ∩ Tr 1 , then (sk , sk+1 ) ∈ Sub1 .
We show by indu tion on k that if (sk , sk+1 ) ∈ G0|after(s0 ) ∩ Tr 1 r Schedule ,
then sk ∈
/ after (s1 ). By indu tion hypothesis, (s2 , sk ) ∈ (G0|after (s0 ) ∩Tr 1 )|after(s1 ) ∪
A0 |after (s0 ) ∪ (G0|after (s0 ) ∩ Tr 2 )]⋆ . Therefore, by Lemma 14, if sk ∈ after(s2 ),
ℓ
then label (sk ) ∈ Labs( 2 cmd2 , ℓ3 ). Therefore, be ause labels are pairwise distin t, if sk ∈ after (s2 ), then label (sk ) ∈
/ Labs(ℓ1 cmd1 , ℓ2 ) r {ℓ2 }. Therefore,
by Lemma 2, if sk ∈ after (s2 ), then (sk , sk+1 ) ∈
/ Tr 1 .
⋆
Hen e, (s1 , s) ∈ [Sub1 |after (s ) ∪A0 |after(s ) ∪(G0 |after (s0 ) ∩Tr 2 )] . By Lemma 7,
1
0
after (s1 ) ⊆ after(s0 ), hen e (s1 , s) ∈ [(Sub1 ∪A0 )|after (s0 ) ∪(G0 |after(s0 ) ∩Tr 2 )]⋆ ⊆
[A1 |after(s0 ) ∪ (G0|after(s0 ) ∩ Tr 2 )]⋆ . Therefore (s1 , s) ∈ Reach2 .
Sin e

3

G-COLLECTING SEMANTICS

25

Lemma 20. Using the above notations, for every (s0 , s) ∈ Reach su h that

s0 ∈ S0 and s′ ∈ S′ , there exists s1 ∈ S1 su h that (s0 , s1 ) ∈ Reach1 , (s1 , s) ∈
Reach2 and (s1 , s) ∈ Ext1 (s0 , s1 ).

Proof.

label(s) ∈ Labs(ℓ1 cmd1 , ℓ2 ).
′
not possible be ause s ∈ S .
In this
Therefore, a ording to Lemma 19 there exists s1 ∈ S1 su h that (s0 , s1 ) ∈
Reach1 , (s1 , s) ∈ Reach2 and (s1 , s) ∈ Ext1 (s0 , s1 )
(s0 , s) ∈ Reach1 , then, a
ase label (s) 6= ℓ3 . This is

If

ording to Lemma 15,

Lemma 21. Using the notations of this se tion, let s0 ∈ S0 , s1 ∈ S1 , s2 ∈ S2 , s

su h that (s0 , s1 ) ∈ Reach1 , (s1 , s2 ) ∈ Reach2 ∩ Ext1 (s0 , s1 ) and (s2 , s) ∈
Ext(s0 , s2 ). Therefore (s1 , s) ∈ Ext1 (s0 , s1 ).
Proof.

Noti e that, by Lemma 7,

after(s2 ) ⊆ after (s1 ) ⊆ after (s0 ).

Re all that:

⋆

Ext(s0 , s2 ) = (G0|after(s0 ) ∩ Tr ) ∪ A0 |after(s0 ) ∪ G0|after(s2 )
⋆

Ext1 (s0 , s1 ) = (G0|after (s0 ) ∩ Tr 1 ) ∪ A0 |after (s0 ) ∪ G0|after(s1 )

By Lemma 17, Ext(s0 , s2 ) =
(G0 |after(s0 ) ∩ Tr 1 ) ∪ (G0 |after(s0 ) ∩ Tr 2 ) ∪
⋆
A0 |after (s0 ) ∪ G0|after (s2 ) . Let T = (G0|after(s0 ) ∩ Tr 2 ) ∪ G0|after(s2 ) . Therefore,

be ause after (s2 ) ⊆ after (s0 ), Ext(s0 , s2 ) = (G0|after(s0 ) ∩ Tr 1 ) ∪ A0 |after (s ) ∪
0
⋆
T|after (s0 ) .

⋆
By Proposition 3, (s2 , s) ∈ (G0|after (s0 ) ∩ Tr 1 ) ∪ A0 |after(s ) ∪ T|after(s1 ) .
0
Be ause after (s2 ) ⊆ after(s1 ) ⊆ after (s0 ), T|after(s1 ) = (G0|after (s1 ) ∩ Tr 2 ) ∪
G0|after (s2 ) . Hen e (s2 , s) ∈ Ext1 (s0 , s1 ). Hen e (s1 , s) ∈ Ext1 (s0 , s1 ); Ext1 (s0 , s1 ) =
Ext1 (s0 , s1 ).

Lemma 22. Using the notations of this se tion, let s0 ∈ S0 , s1 ∈ S1 , s2 ∈ S2 , s

su h that (s0 , s1 ) ∈ Reach1 , (s1 , s2 ) ∈ Reach2 ∩ Ext1 (s0 , s1 ) and (s2 , s) ∈
Ext(s0 , s2 ). Therefore (s2 , s) ∈ Ext2 (s1 , s2 ).
Proof.

Noti e that, by Lemma 7,

Re all that

after(s2 ) ⊆ after (s1 ) ⊆ after (s0 ).


⋆
Ext(s0 , s2 ) = (G0|after(s0 ) ∩ Tr ) ∪ A0 |after(s0 ) ∪ G0|after(s2 )
⋆

Ext2 (s1 , s2 ) = (G1|after (s1 ) ∩ Tr 2 ) ∪ A1 |after (s1 ) ∪ G1|after(s2 )
Sin e (s2 , s) ∈ Ext(s0 , s2 ), A0 ⊆ A1 , G0 ⊆ A1 , and after (s1 ) ⊆ after(s0 )
there exists s3 , . . . , sn su h that sn = s and for all k ∈ {3, . . . , n − 1},
(sk , sk+1 ) ∈ (G1|after (s0 ) ∩ Tr ) ∪ A1 |after (s1 ) ∪ G1|after (s2 ) .
Due to Lemma 17, for all k ∈ {3, . . . , n − 1}, (sk , sk+1 ) ∈ (G1|after (s0 ) ∩
Tr 1 ) ∪ (G1|after(s0 ) ∩ Tr 2 ) ∪ A1 |after (s1 ) ∪ G1|after (s2 ) .

3

G-COLLECTING SEMANTICS

26


⋆
(s1 , s2 ) ∈ Reach2 , (s1 , s2 ) ∈ (G1|after (s1 ) ∩ Tr 2 )A1 |after (s1 ) ⊆
⋆

(G1|after (s0 ) ∩ Tr 2 ) ∪ (G1|after (s0 ) ∩ Tr 2 ) ∪ A1 |after(s1 ) ∪ G1|after(s2 ) .
ℓ
Hen e, by Proposition 3 applied on the statement 1 cmd 1 , ℓ2 , for all k ∈
{3, . . . , n − 1}, (sk , sk+1) ∈ (G1|after (s0 ) ∩ Tr 1 ) ∪ (G1|after (s1 ) ∩ Tr 2 ) ∪ A1 |after(s1 ) ∪
G1|after (s2 ) .
Given that (G1|after (s0 ) ∩ Tr 1 ) = (G1|after (s0 )rafter (s0 ) ∩ Tr 1 ) ∪ (G1|after (s1 ) ∩ Tr 1 )
and G1|after (s2 ) ∩ Tr 1 ⊆ G1|after (s2 ) , by Proposition 3 applied on the stateℓ
ment 2 cmd 2 , ℓ3 , we on lude that for all k ∈ {3, . . . , n − 1}, (sk , sk+1 ) ∈
(G1|after (s0 )rafter (s1 ) ∩ Tr 1 ) ∪ (G1|after(s1 ) ∩ Tr 2 ) ∪ A1 |after(s1 ) ∪ G1|after(s2 ) . Let k0
su h that (sk0 , sk0 +1 ) ∈ (G1|after(s0 )rafter (s1 ) ∩ Tr 1 ) r G1|after (s2 ) . By Lemma 21,
(s1 , sk0 ) ∈ Ext1 (s0 , s1). Therefore (sk0 , sk0 +1 ) ∈ Sub1 .
Hen e (s2 , s) ∈
Sub1|after (s0 )rafter (s1 ) ∪ (G1|after(s1 ) ∩ Tr 2 ) ∪ A1 |after (s0 ) ∪
⋆
G1|after (s2 ) . Be ause Sub1|after(s0 )rafter (s1 ) ⊆ A|after s1 , we on lude that (s2 , s) ∈
Ext2 (s1 , s2 ).
Be ause

′
To prove the Property 1 of Theorem 1, we have to prove that Q2 > Q . We
′
′
′
laim that (a) S ⊆ S2 (b) Self ⊆ Self1 ∪Self2 ( ) Par ⊆ Par1 ∪Par2 ∪Sub1
′
(d) Sub ⊆ Sub1 ∪ Sub2 . Using this laims and the denition of the semanti s
 
· , we on lude that Q2 > Q′ .
Now, we prove these

laims:

Claim 5. Using the notations of this se tion, S′ ⊆ S2 .

Proof.

(s0 , s) ∈ Reach′ and
label(s) = ℓ3 . A ording to Lemma 20 there exists s1 ∈ S1 su h that (s1 , s) ∈
Reach2 . Therefore s ∈ S2 .
Let

s ∈ S′ ,

so there exists

s0 ∈ S

su h that

Claim 6. Using the notations of this se tion, Self′ ⊆ Self1 ∪ Self2 .
Proof.

(s, s′ ) ∈ Self′ .
(s0 , s) ∈ Reach′ .
Let

So

(s, s′) ∈ Tr ,

and there exists

s0 ∈ S

su h that

(s0 , s) ∈ Reach1 and label(s) 6= ℓ2 , or there
(s0 , s1 ) ∈ Reach1 and (s1 , s) ∈ Reach2 .
ℓ
In the rst ase, a ording to Lemma 15, label (s) ∈ Labs( 1 cmd 1 , ℓ2 ).
′
Sin e label(s) 6= ℓ2 and by Lemma 18, (s, s ) ∈ Tr 1 . Hen e, by denition,
(s, s′ ) ∈ Self1
′
ℓ
In the se ond ase, by Lemma 14, label(s ) ∈ Labs( 2 cmd 2 , ℓ3 ). Sin e
′
′
(s, s ) ∈ Tr , by Lemma 18 (s, s ) ∈ Tr 2 . Given that s ∈ ReachhS1 i and
(s, s′ ) ∈ Tr 2 , we on lude that (s, s′ ) ∈ Self2 .
A

exists

ording to Lemma 19 either

s1 ∈ S1

su h that

3

G-COLLECTING SEMANTICS

27

Claim 7. Using the notations of this se tion Par′ ⊆ Par1 ∪ Par2 ∪ Sub1 .
Proof.
and
A

s2

Let
su

(s, s′ ) ∈ Par′ . Therefore, (s, s′) ∈ Tr and there exists s0 ∈ S0
′
h that (s0 , s2 ) ∈ Reach , (s2 , s) ∈ Schedule and s ∈ after(s0 ).

ording to Lemma 19 there are two

ases:

ase: (s0 , s2 ) ∈ Reach1 and label (s2 ) 6= ℓ2 . Then, using the fa t
Schedule ⊆ Tr 1 , (s0 , s) ∈ (Tr 1 ∪ A0 |after (s0 ) )⋆ . Be ause s ∈ after (s0 ), by
ℓ
Lemma 14, label (s) ∈ Labs( 1 cmd 1 , ℓ2 ) r {ℓ2 }. Hen e, a ording to Lemma
′
′
18, (s, s ) ∈ Tr 1 . We on lude that (s, s ) ∈ Par1 .
Se ond ase: There exists s1 ∈ S1 su h that (s0 , s1 ) ∈ Reach1 , (s1 , s2 ) ∈
Reach2 and (s1 , s2 ) ∈ Ext1 (s0 , s1 ). Hen e (s1 , s) ∈ Ext1 (s0 , s1 ); Schedule =
Ext1 (s0 , s1 ).
If s ∈ after (s1 ), then, be ause (s1 , s) ∈ Reach2 ; Schedule , by Lemma 14,
label(s) ∈ Labs(ℓ2 cmd 2 , ℓ3 ). So, in this ase, by Lemma 18, (s, s′ ) ∈ Tr 2 and
′
then (s, s ) ∈ Par2 .
Let us onsider the ase s ∈
/ after (s1 ). Given that (s0 , s1 ) ∈ Reach,
(s1 , s) ∈ Ext1 (s1 , s2 ), so by Proposition 3, (s, s′ ) ∈ Tr 1 . Hen e, (s, s′ ) ∈
Sub1 .
First

that

Claim 8. Using the notations of this se tion Sub′ ⊆ Sub1 ∪ Sub2 .
Proof.

(s, s′ ) ∈ Sub′ . Then, there exists s0 and s2 su h that (s0 , s2 ) ∈
Reach and (s2 , s) ∈ Ext(s0 , s2 ). A ording to Lemma 20, there exists s1 ∈ S1
su h that (s0 , s1 ) ∈ Reach1 and (s1 , s2 ) ∈ Reach2 and (s1 , s2 ) ∈ Ext1 (s0 , s1 ).
By Lemma 21 and Lemma 22, (s1 , s) ∈ Ext1 (s0 , s1 ) and (s2 , s) ∈ Ext2 (s1 , s2 ).
Let us onsider the ase s ∈
/ after(s1 ). Be ause s ∈ after(s0 ), then
s ∈ after (s0 ) r after(s1 ). Furthermore, given that (s0 , s1 ) ∈ Reach1 and
(s1 , s) ∈ Reach2 , by Proposition 3, (s, s′ ) ∈ Tr 1 . We on lude that (s, s′ ) ∈
Sub1 .
Let us onsider the ase s ∈ after (s1 ). Be ause s ∈ after (s0 ) r after(s2 ),
s ∈ after(s1 ) r after (s2 ). By Lemma 14, label (s) ∈ Labs(ℓ2 cmd 2 , ℓ2 ). Hen e,
′
′
by Lemma 18, (s, s ) ∈ Tr 2 and therefore, (s, s ) ∈ Sub2 .
Let

′

3.5.2 Proof of Property 2 of Theorem 1
if (cond)then{ℓ2 cmd 1 }else{ℓ3 cmd 2 }, ℓ4
Q0 = hS0 , G0 , A0 i

In this se tion, we onsider a ommand
and an initial

onguration

ℓ1

3

G-COLLECTING SEMANTICS

28



hS′ , G′ , A′ i = ℓ1 if (cond )then{ℓ2 cmd}else{ℓ3 cmd }, ℓ4 hS, G, Ai.
hS+ , G+ , A+ i = ℓ1 guardcond
 , ℓ2 hS, G, Ai.
hS1 , G1 , A1 i = ℓ2 cmd 1 , ℓ4 hS+ , G+, A+ i.
hS¬ , G¬ , A¬ i = ℓ1 guard¬cond
 , ℓ3 hS, G, Ai.
hS2 , G2 , A2 i = ℓ3 cmd 1 , ℓ4 hS¬ , G¬ , A¬ i.
Tr = Tr ℓ1 if (cond )then{ℓ2 cmd}else{ℓ3 cmd},ℓ4 .

Let
Let
Let
Let
Let
Let

Lemma 23. Tr ℓ1 if (cond )then{ℓ2 cmd}else{ℓ3 cmd},ℓ4 = Tr ℓ1 guardcond ,ℓ2 ∪ Tr ℓ2 cmd 1,ℓ4 ∪
Tr ℓ1 guard ¬cond ,ℓ3 ∪ Tr ℓ3 cmd 1 ,ℓ4 .
Lemma 24. If (s0 , s) ∈ Reach and s0 ∈ S0 , then, one of the three folowing
properties hold:
1. s ∈ interfereA0 ({s0 }),
2. or there exists s1 ∈ S+ su h that (s1 , s) ∈ Reach1 ∩ Ext+ (s0 , s1 )
3. or there exists s1 ∈ S¬ su h that (s1 , s) ∈ Reach2 ∩ Ext¬ (s0 , s1 )
Proof.

s ∈
/ interfere A0 ({s0 }). Be ause (s0 , s) ∈
Reach, (s0 , s) ∈ [(G0|after (s0 ) ∩ Tr ) ∪ A0 |after (s0 ) ]⋆ .
⋆
′
′
Therefore, there exists s0 and s1 su h that (s0 , s0 ) ∈ (A0 |after (s ) ∪Schedule) ,
0
(s′0 , s1 ) ∈ G0|after(s0 ) ∩ Tr and (s1 , s) ∈ [(G0|after(s0 ) ∩ Tr ) ∪ A0 |after (s0 ) ]⋆ . Be′
ause (s0 , s1 ) ∈ G0|after(s0 ) ∩ Tr , s ∈ after (s0 ). By Lemma 11, thread (s0 ) =
thread (s′0 ). By Lemma 13, label (s0 ) = label (s′0 ) = ℓ1 . Therefore, due to
′
′
Lemmas 1 and 23, (s0 , s1 ) ∈ Tr ℓ1 guard cond,ℓ2 ∪ Tr ℓ1 guard¬cond ,ℓ3 . Either (s0 , s1 ) ∈
′
Tr ℓ1 guard cond,ℓ2 or (s0 , s1 ) ∈ Tr ℓ1 guard ¬cond,ℓ3 .
In the rst ase, by Lemma 1, thread (s0 ) = thread (s1 ) and label (s1 ) = ℓ2 .
Therefore, (s0 , s1 ) ∈ Reach+ and s1 ∈ S+ . There exists a sequen e s2 , sn su h
that sn = s and ∀k ∈ {1, . . . n − 1}, (sk , sk+1 ) ∈ (G0|after (s0 ) ∩ Tr ) ∪ A0 |after(s ) .
0
Let us prove by indu tion on k , that ∀k ∈ {1, . . . n}, (sk , sk+1 ) ∈ (G0|after(s1 ) ∩
Tr ℓ2 cmd,ℓ4 ) ∪ A0 |after(s0 ) . Let us onsider the ase (sk , sk+1 ) ∈ G0|after (s0 ) ∩ Tr .
⋆
By indu tion hypothesis (s1 , sk ) ∈ [(G0|after (s1 ) ∩ Tr ℓ2 cmd,ℓ4 ) ∪ A0 |after (s ) ] .
0
Hen e, by Proposition 3, either (sk , sk+1 ) ∈ Tr ℓ1 guard (cond ),ℓ2 or sk ∈ after(s1 ).
If (sk , sk+1 ) ∈ Tr ℓ1 guard(cond ),ℓ2 and sk ∈ after (s1 ) then (sk , sk+1 ) ∈ Sub+ .
This is ontradi tory with Claim 2. Therefore sk ∈ after (s1 ). By Lemma
ℓ
14, label (sk ) ∈ Labs( 2 cmd 1 , ℓ4 ). Hen e, by Lemmas 1 and 23, (s1 , sk ) ∈
Tr ℓ2 cmd,ℓ4 .
∗
We on lude that (s1 , s) ∈ [(G0|after (s1 ) ∩Tr ℓ2 cmd,ℓ4 )∪A0 |after (s ) ] ⊆ Reach1 ∩
0
Ext+ (s0 , s1 ).
Let us

onsider the

ase

3

G-COLLECTING SEMANTICS

The se ond

29

ase is similar.

Claim 9. S′ ⊆ S1 ∪ S2
Proof.

s ∈ S′ . Therefore there exists s0 ∈ S0 su h that (s0 , s) ∈ Reach
and label (s) = ℓ4 6= ℓ1 . Hen e, due to Lemma 13, s ∈
/ interfereA0 {s0 }.
A ording to Lemma 24, there exists s1 su h that either (1) s1 ∈ S+
and (s1 , s) ∈ Reach1 ∩ Ext+ (s0 , s1 ), (2) or, s1 ∈ S¬ and (s1 , s) ∈ Reach2 ∩
Ext¬ (s0 , s1 ).
In the rst ase, by denition, s ∈ S1 and in the se ond ase s ∈ S2
Let

Claim 10. Self ⊆ Self+ ∪ Self1 ∪ Self¬ ∪ Self2 .
Proof.

Let

(s, s′ ) ∈ Self.

Reach.
Let us

ℓ1 .

onsider the

ase

Then, there exists

s0 ∈ S0 )

su h that

(s0 , s) ∈

s ∈ interfereA0 ({s0 }). By Lemma 13, label(s) =
(s, s′ ) ∈ Tr ℓ1 guardcond ,ℓ2 ∪ Tr ℓ1 guard ¬cond,ℓ3 .

Hen e, by Lemmas 1 and 23,
′
Hen e, (s, s ) ∈ Self+ ∪ Self¬ .

s ∈
/ interfereA0 ({s0 }), then, there exists
s1 su h that either (1) s1 ∈ S+ and (s1 , s) ∈ Reach1 ∩ Ext+ (s0 , s1 ), (2) or,
s1 ∈ S¬ and (s1 , s) ∈ Reach2 ∩ Ext¬ (s0 , s1 ).
ℓ
In the rst ase, by Lemma 14, label (sk ) ∈ Labs( 2 cmd 1 , ℓ4 ). Hen e, by
′
Lemmas 1 and 23, (s1 , sk ) ∈ Tr ℓ2 cmd,ℓ4 and therefore (s, s ) ∈ Self1 .
′
In the se ond ase, we similarly on lude that (s, s ) ∈ Self2 .
A

ording to Lemma 24, if

Claim 11. Par ⊆ Par1 ∪ Par2 .
Proof.

(s, s′ ) ∈ Par. Therefore, there exists s0 ∈ S0 and s2 su h that
(s0 , s2 ) ∈ Reach and (s2 , s) ∈ Schedule and s ∈ after (s0 ). Noti e that
thread (s0 ) = thread (s2 ) 6= thread (s).
Assume by ontradi tion that s2 ∈ interfere ( {s0 }). Hen e, due to Lema
11, thread (s) = thread (s0 ). This is ontradi tory.
Therefore, a ording to Lemma 24, there exists s1 su h that either (1) s1 ∈
S+ and (s1 , s) ∈ Reach1 ∩ Ext+ (s0 , s1 ), (2) or, s1 ∈ S¬ and (s1 , s) ∈ Reach2 ∩
Ext¬ (s0 , s1 ).In the two ases, by Lemma 12, s ∈ after(s1 ).
ℓ
In the rst ase, by Lemma 14, label(s) ∈ Labs( 2 cmd 1 , ℓ4 ) and therefore,
′
′
by Lemmas 23 and 1, (s, s ) ∈ Tr ℓ2 cmd 1 ,ℓ4 . Hen e, (s, s ) ∈ Par1
′
In the se ond ase, we similarly on lude that (s, s ) ∈ Par2 .
Let

Claim 12. Sub ⊆ Sub1 ∪ Sub2 .

3

G-COLLECTING SEMANTICS

Proof.

30

(s, s′ ) ∈ Sub. Therefore, there exists s0 ∈ S0 and s2 ∈ S′ su h
that (s0 , s2 ) ∈ Reach and (s2 , s) ∈ Ext(s0 , s2 ) and s ∈ after (s0 ) r after(s2 ).
Noti e that thread (s0 ) = thread (s2 ) 6= thread (s).
Assume by ontradi tion that s2 ∈ interfere ( {s0 }). Hen e, due to
′
Lemma 13, label (s2 ) = ℓ1 . This is ontradi tory with s2 ∈ S .
Therefore, a ording to Lemma 24, there exists s1 su h that either (1) s1 ∈
S+ and (s1 , s) ∈ Reach1 ∩ Ext+ (s0 , s1 ), (2) or, s1 ∈ S¬ and (s1 , s) ∈ Reach2 ∩
Ext¬ (s0 , s1 ).In the two ases, by Lemma 12, s ∈ after(s1 ).
In the rst ase, be ause s ∈
/ after (s2 ), by Proposition 3, (s, s′ ) ∈ Tr ℓ1 cmd 1 ,ℓ2 .
′
Hen e, (s, s ) ∈ Sub1
′
In the se ond ase, we similarly on lude that (s, s ) ∈ Sub2 .
Let

Property 2 of Theorem 1 is a straightforward

onsequen e of Claims 9,

10, 11, 12.

3.5.3 Proof of Property 3 of Theorem 1
In this se tion, we
tial
Let
Let
Let
Let
Let
Let
Let
Let
Let
Let

onsider a

ommand

ℓ1

while(cond ){ℓ2 cmd }, ℓ3

and an ini-

Q0 =
 ℓhS0 , G0 , A0 i. ℓ

Q = hS , G , A i = 1 while(cond){ 2 cmd }, ℓ3 Q0 .
Qω = hSω , Gω , Aω i =loop↑ω (Q0 ).

ℓ2
Q′′ = hS′′ , G′′ , A′′ i = ℓ1 while(cond ){
cmd }, ℓ3 Qω .
ℓ1
K = [Reach, Ext, Self,
while(cond
){ℓ2 cmd }, ℓ3 Qω .
 ℓPar, Sub] =

Q+ = hS+ , G+ , A+ i = 1 guard(cond), ℓ2 (Qω).
K+ = [Reach+ , Ext+ , Self+ , Par+ , Sub+ ] = ℓ1 guard(cond),
 ℓ ℓ2 (Qω ).
2
Kcmd = [Reachcmd , Ext
cmd , ℓ1 (Q+ ).
 ℓ cmd , Selfcmd , Parcmd
 , Subcmd ] =
1
Q¬ = hS¬ , G¬ , A¬ i =
.
guard(¬cond ), ℓ3 Q
ω
K¬ = [Reach¬ , Ext¬ , Self¬ , Par¬ , Sub¬ ] = ℓ1 guard(¬cond ), ℓ3 Qω .
Tr = Tr ℓ1 while(cond ){ℓ2 cmd},ℓ3 .
onguration
′
′
′ ′

Lemma 25.

Tr ℓ1 while(cond ){ℓ2 cmd},ℓ3 = Tr ℓ1 guard (¬cond ),ℓ3 ∪ Tr ℓ1 guard(cond ),ℓ2 ∪ Tr ℓ2 cmd ,ℓ1
Noti e that, by denition,

Q0 6 Qω

Lemma 26. We use the above notations. Let s0 , s1 , . . . , sn , . . . , sm a sequen e

of states su h that (s0 , sm ) ∈ Reachω , (s0 , sn) ∈ Reachω , sn ∈ Sω and for all
k ∈ {0, . . . , m − 1}, (sk , sk+1) ∈ (Gω |after(s0 ) ∩ Tr ) ∪ Aω |after (s0 ) .
Therefore, (sn , sm ) ∈ Reachω .

3

G-COLLECTING SEMANTICS

Proof.

For all

31

k , (sk , sk+1) ∈ (Gω|after (sn ) ∩ Tr ) ∪ (Gω |after(s0 )rafter (sn ) ∩ Tr ) ∪

Aω |after (s0 ) .
Let k0 > n su h that (sk0 , sk0 +1 ) ∈ (Gω |after (s0 )rafter (sn ) ∩ Tr ). Noti e that
(sn , sk0 ) ∈ Extω (s0 , sn ) and sk0 ∈ after (s0 ) r after (sn ). Hen e, (sk0 , sk0 +1 ) ∈
Subω ⊆ Aω . Therefore (sk0 , sk0 +1 ) ∈ Aω |after(s1 ) .
In addition to this, a ording to Lemma 15, after(sn ) ⊆ after (s0 ), so, for
all k > n, (sk , sk+1 ) ∈ (Gω|after (sn ) ∩ Tr ) ∪ Aω |after (s ) .
0

Lemma 27. Using the notations of this se tion, if s ∈ ReachhS0 i, then, there

exists s0 ∈ Sω su h that:

1. either (s0 , s) ∈ Reach¬ ,
2. or there exists s1 ∈ S+ su h that (s0 , s1 ) ∈ Reach+ and (s1 , s) ∈
Reachcmd and label (s) 6= ℓ1 .
Proof.

s ∈ ReachhS0 i.

s0 , . . . , sn of minimal
sn = s, (2) s0 ∈ Sω ,
(3) for all k ∈ {0, . . . , n − 1}, (sk , sk+1 ) ∈ (Gω |after(s0 ) ∩ Tr ) ∪ Aω |after(s ) . A
0
su h sequen e exists be ause S0 ⊆ Sω .
If for all k ∈ {0, . . . , n−1}, (sk , sk+1 ) ∈ Schedule ∪Aω |after(s ) then (s0 , s) ∈
0
Reach+ ∩ Reach¬ ⊆ Reach¬ .
Let us assume, from now, that there exists k ∈ {0, . . . , n − 1} su h that
(sk , sk+1 ) ∈ Gω|after (s0 ) ∩ Tr ℓ1 while(cond ){ℓ2 cmd},ℓ3 r Schedule . Let k0 the smallest
su h k .
Therefore (sk0 , sk0 +1 ) ∈ Gω|after (s0 ) , so, sk0 ∈ after (s0 ). A ording to
Lemma 11, thread (s0 ) = thread (sk0 ). By Lemma 13, label(s0 ) = label(sk0 ).
/ Tr ℓ2 cmd,ℓ1 . ThereBut label(s0 ) = ℓ1 , therefore, by Lemma 2, (sk0 , sk0 +1 ) ∈
fore, by Lemma 25, either (sk0 , sk0 +1 ) ∈ Tr ℓ1 guard(¬cond ),ℓ3 or (sk0 , sk0 +1 ) ∈
Tr ℓ1 guard (cond ),ℓ2 .
In the rst ase, by Lemma 5, label(sk0 +1 ) = ℓ3 . Let us prove by indu tion on k that for all k > k0 , (sk , sk+1 ) ∈ Aω |after (s ) ∪ Schedule . By
0
⋆
indu tion hypothesis (sk0 , sk ) ∈ [Aω |after (s ) ∪ Schedule] . Let us onsider the
0
ase (sk , sk+1 ) ∈ Gω|after (s0 ) ∩ Tr . Therefore sk ∈ after (s0 ), then by Lemma
11, thread (sk ) = thread (sk0 +1 ). By Lemma 13, label (sk ) = label(sk0 +1 ) = ℓ3 .
So, by Lemma 2, (sk , sk+1 ) ∈ Schedule . Hen e (s0 , s) ∈ Reach¬ .
In the se ond ase, (s0 , sk0 +1 ) ∈ Reach+ and therefore, by Lemma 5,
sk0 +1 ∈ S+ . Either there exists k1 > k0 su h that (sk1 , sk1 +1 ) ∈ G|after (s0 ) ∩
(Tr ℓ1 guard (¬cond ),ℓ3 ∪ Tr ℓ1 guard(cond ),ℓ3 ) or there does not exists a su h k1 .
Let

We

onsider a sequen e

length su h that the following properties hold:

(1)

3

G-COLLECTING SEMANTICS

32

k1 exists, therefore, by Lemma 5, label(sk0 ) =
ℓ1 . A ording to Lemma 14, thread (s) = thread (s0 ). Hen e, (s0 , sk1 ) ∈
Reachω . So, by Lemma 26, (sk1 , sn ) ∈ Reachω . This is ontradi tory with
the minimality of the path s1 , . . . , sn . Therefore k1 does not exists.
Hen e, for all k > k0 , (sk , sk+1 ) ∈ (Gω |after(s0 ) ∩ Tr ℓ2 cmd,ℓ1 ) ∪ Aω |after (s ) . A 0
ording to proposition 3, for all k > k0 , (sk , sk+1 ) ∈ (Gω |after (s1 ) ∩ Tr ℓ2 cmd,ℓ1 ) ∪
Aω |after (s0 ) . Therefore, (sk0 , s) ∈ Reachω
Assume by ontradi tion that

Claim 13. Using the notation of this se tion S′ ⊆ S¬ .
Proof.

Let

Hen e, a
a

s ∈ S′ ,

ording to Lemma 27,

Hen e

s ∈ ReachhS0 i. Furthermore, label(s) = ℓ3 .
s1 , (s1 , s) ∈
/ Reachω . Therefore,
there exists s0 ∈ Sω su h that (s0 , s) ∈ Reach¬ .

therefore,

ording to Lemma 15, for all

s ∈ S¬ .

Claim 14. Self ⊆ Self¬ ∪ Self+ ∪ Selfcmd
Proof.

(s, s′ ) ∈ Self. A
Tr ℓ1 guard (cond ),ℓ2 ∪ Tr ℓ2 cmd,ℓ1 .
Let

ording to Lemma 25,

(s, s′ ) ∈ Tr ℓ1 guard(¬cond ),ℓ3 ∪

(s, s′ ) ∈ Tr ℓ1 guard (¬cond ),ℓ3 ∪ Tr ℓ1 guard (cond ),ℓ2 . Due
to Lemma 5, label (s) = ℓ1 Hen e, a ording to Lemma 27, either (s0 , s) ∈
Reach¬ or there exists s1 ∈ S+ su h that (s1 , s) ∈ Reachcmd ( ontradi tion
with Lemma 15 and label (s) = ℓ1 ). A ording to Lemma 16, either label(s) =
ℓ2 6= ℓ1 ( ontradi tion) or s ∈ interfereA0 (S0 ) ⊆ Reach¬ hSω i ∩ Reach+ hSω i.
′
′
Therefore either (s, s ) ∈ Self¬ or (s, s ) ∈ Self+ .
′
Let us onsider the ase (s, s ) ∈ Tr ℓ2 cmd,ℓ1 . Therefore, a ording to
ℓ
′′
Lemma 1, label (s) ∈ Labs( 2 cmd , ℓ1 ) r {ℓ1 }. If s ∈ Reach¬ hSω i, then, by
′′
Lemma 16, label (s ) ∈ {ℓ1 , ℓ3 }. Hen e, s ∈
/ Reach¬ hSω i. So, by Lemma
27, there exists s ∈ S0 and s1 ∈ S+ su h that (s0 , s1 ) ∈ Reach+ and
(s1 , s) ∈ Reachcmd . A ording to Proposition 3, (s, s′ ) ∈ after(s1 ) and there′
fore (s, s ) ∈ Selfcmd .
Let us

onsider the

ase

Claim 15. Par ⊆ Parcmd
Proof.

(s, s′ ) ∈ Par. There exists s0 and s2 su h that (s0 , s2 ) ∈ Reachω .
By Lemma 16, either (s0 , s2 ) ∈ Reach¬ or there exists s1 ∈ S+ su h that
(s0 , s1 ) ∈ Reach+ and (s1 , s2 ) ∈ Reachcmd and label (s2 ) 6= ℓ2 .
In the rst ase, be ause s ∈ after (s0 ), by Lemma 11, thread (s) =
thread (s0 ). But, by denition of Schedule and Reach¬ , thread (s2 ) 6= thread (s)
and thread (s0 ) = thread (s2 ). This is ontradi tory.
Let

3

G-COLLECTING SEMANTICS

33

s ∈ after s1 . Be ause thread (s) 6=
thread (s0 ) = thread (s2 ), by Lemma 14, label(s) ∈ Labs(ℓ2 cmd , ℓ1 ) r {ℓ2 }.
′
′
Therefore, by Lemmas 25 and 5, (s, s ) ∈ Tr ℓ2 cmd,ℓ1 . Hen e (s, s ) ∈ Parcmd
In the se ond

ase, by Proposition 3,

Claim 16. Sub ⊆ Sub¬
Proof.

(s, s′) ∈ Sub. Therefore, there exists s0 Sω and s1 ∈ S′ su h that
(s0 , s1 ) ∈ Reach and (s1 , s) ∈ Ext(s0 , s1 ).
Noti e that label (s1 ) = ℓ3 , therefore, a ording to Lemma 15, s1 ∈
/
Reach+ ; Reachcmd hSω i. hen e, by Lemma 27, (s0 , s1 ) ∈ Reach¬ .
(s1 , s) ∈ Ext(s0 , s1 ) ⊆ (Gω |after (s0 ) ∩ Tr ) ∪ Aω |after (s0 ) ∪ Gω|after (s1 ) . By
Proposition 3, (s1 , s) ∈ (Gω |after (s0 ) ∩ Tr ℓ1 guard (¬cond ),ℓ2 ) ∪ (Gω |after(s1 ) ∩ Tr r
Tr ℓ1 guard (¬cond ),ℓ2 ) ∪ Aω |after (s0 ) ∪ Gω |after (s1 ) = Ext¬ (s1 , s2 ).
Let

Property 3 of Theorem 1 is a straightforward

onsequen e of Claims 13,

14, 15 and 16.

3.5.4 Proof of Property 4 of Theorem 1
Let
Let
Let
Let
Let
Let
Let
Let
Let

Q0 = hS0 , G0 , A0 i a onguration.

Q′ = hS′ , G′ , A′ i = ℓ1 create(ℓ2 cmd), ℓ3 (Q0 )
ℓ1
ℓ2
K = [Reach, Ext, Self,
 ℓ Par, Sub] =  create( cmd ), ℓ3 (Q0 )
Q1 = hS1 , G1 , A1 i = 1 spawn(ℓ2 ), ℓ3 (Q0 ) 
K1 = [Reach1 , Ext1 , Self1 , Par1 , Sub1 ] = ℓ1 spawn(ℓ2 ), ℓ3 (Q0 )
Q2 = hS2 , G2 , A2 i = init- hildℓ2 (Q1 )
G∞ = guarantee ℓ2 cmd,ℓ∞ (Q2 )

K3 = [Reach3 , Ext3 , Self3 , Par3 , Sub3 ] = ℓ2 cmd , ℓ∞ hS2 , G∞ , A2 i
Q3 = hS3 , G3 , A3 i = ombineQ0 (G∞ ) Let Tr = Tr ℓ1 create (ℓ2 cmd),ℓ3

Lemma 28. Tr ℓ1 create(ℓ2 cmd),ℓ3 = Tr ℓ1 spawn(ℓ2 ),ℓ3 ∪ Tr ℓ2 cmd,ℓ∞

Lemma 29. Let T a set of transitions. Let s0 , s1 , s2 , s and s′ su h that

(s0 , s1 ) ∈ Reach1 , s2 ∈ s hedule- hild {s1 }, label (s1 ) = ℓ3 , (s2 , s) ∈ T ⋆ and
s ∈ after(s0 ).
Therefore, s ∈ after (s1 ) ∪ after (s2 ).

Proof.

′
′
′
ording to Lemma 16, there exists s0 and s1 su h that, s0 ∈
interfereA0 {s0 }, (s′0 , s′1 ) ∈ Tr ℓ1 spawn(ℓ2 ),ℓ3 rSchedule , and s1 ∈ interfereA0 {s′1 }.
′
′
By Lemmas 11 and 1, thread (s0 ) = thread (s0 ) = thread (s1 ) = thread (s1 ).
A

3

G-COLLECTING SEMANTICS

34

i0 = thread (s0 ) and i = thread (s).
′
′
′′
Let g0 , g0 , j , g1 and g su h that, respe tively, the genealogy of s0 , s0 , s0 ,
s1 , s2 , s is g0 , g0 · g0′ , g0 · g0′ · (i0 , ℓ2 , j), g0 · g0′ · (i0 , ℓ2 , j) · g1, g0 · g0′ · (i0 , ℓ2 , j) · g1 ,
g0 · g0′ · (i0 , ℓ2 , j) · g1 · g . Noti e that s1 and s2 have the same genealogy.
′
∗
Be ause (s0 , s0 ) ∈ [A0 |after (s ) ∪ Schedule] , by Lemma 10, desc g ′ {i0 } =
0
0
{i0 }.
′′
∗
Be ause (s1 , s1 ) ∈ [A0 |after (s ) ∪Schedule] , by Lemma 10, desc (i0 ,ℓ2 ,j)·g1 {i0 } =
0
desc (i0 ,ℓ2 ,j) {i0 } = {i0 , j}.
By denition of desc , desc g ′ ·(i0 ,ℓ2 ,j)·g1 ·g ({i0 }) = desc g [desc (i0 ,ℓ2 ,j)·g1 (desc g ′ {i0 })] =
0
0
desc g {i0 , j} By denition of desc , desc g0′ ·(i0 ,ℓ2 ,j)·g1·g ({i0 }) = desc g ({i0 }) ∪
desc g ({j}).
Be ause s ∈ after (s0 ), i ∈ desc g ′ ·(i0 ,ℓ2 ,j)·g2 ·g ({i0 }). Therefore either i ∈
0
desc g ({i0 }) or i ∈ desc g ({j}). If i ∈ desc g ({i0 }) then s ∈ after(s1 ). If
i ∈ desc g ({j}) then s ∈ after (s2 ).
Let

Lemma 30. Let s0 , s1 , s2 , s and s′ su h that (s0 , s1 ) ∈ Reach1 , s2 ∈

s hedule- hild{s1 }, label (s1 ) = ℓ3 , (s2 , s) ∈ (G0 ∪ A0 )⋆|after (s ) and (s, s′ ) ∈
1
G0|after (s0 ) ∩ Tr .
Therefore, s ∈ after (s2 ) (i.e., (s, s′ ) ∈ G0|after(s2 ) ∩ Tr ).

Proof.

s ∈ after (s1 ) ∪ after(s2 ). Assume by ontradi tion
that s ∈ after (s1 ). Therefore, by Lemma 11, thread (s) = thread (s1 ) and by
Lemma 13, label (s) = label(s1 ) = ℓ3 . This is ontradi tory with Lemma 1
whi h implies label (s) 6= ℓ3 .
Due to Lemma 29,

Lemma 31. If (s0 , s) ∈ Reach then:
• either s ∈ interfereA0 (s0 ) and label(s) = ℓ1
• or there exists s1 , s2 , s3 su h that (s0 , s1 ) ∈ Reach1 , (s1 , s2 ) ∈ Schedule ,
(s2 , s3 ) ∈ Reach3 ∩Ext1 (s0 , s1 ), (s3 , s) ∈ Schedule and s2 ∈ s hedule- hild {s1 }.
Furthermore label(s1 ) = label(s) = ℓ3 and s ∈ interfereG0 ∪A0 {s1 }.

Proof.

(s0 , s) ∈ [A0 |after (s0 ) ∪ Schedule]∗
13, label (s) = ℓ1 .

If

Lemma

then

s ∈ interfereA0 (s0 )

and by

onsider the other ase: (s0 , s) ∈
/ [A0 |after(s0 ) ∪ Schedule]∗ .
′
′
∗
Therefore, there exists s0 and s1 su h that (s0 , s0 ) ∈ [A0 |after (s ) ∪ Schedule] ,
0
(s′0 , s1 ) ∈ (G0|after(s0 ) ∩ Tr ) and (s1 , s) ∈ [(G0|after(s0 ) ∩ Tr ) ∪ A0 |after(s0 ) ]⋆ .
Then, let us

3

G-COLLECTING SEMANTICS

35

s′0 ∈ after (s0 ), thread (s′0 ) = thread (s0 ). A ′
ording to Lemma 5, thread (s1 ) = thread (s0 ) = thread (s0 ) and label (s1 ) = ℓ3 .
Therefore (s0 , s1 ) ∈ Reach1 .
′
′
Let (i1 , P1 , σ1 , g1 ) = s1 . Let g1 and j su h that g1 · (i, ℓ2 , j) = g1 . Let s2 =
(j, P1 , σ1 , g1 ). Therefore, s2 ∈ s hedule- hild {s1 } and (s1 , s2 ) ∈ Schedule .
Let (i, P, σ, g) = s and s3 = (j, P, σ, g). Therefore, (s3 , s) ∈ Schedule .
Given that Schedule ⊆ A0 ∩G0 ∩Tr , we on lude that (s2 , s3 ) ∈ [(G0|after(s0 ) ∩
Tr )∪A0 |after (s0 ) ]⋆ . Using Lemma 30 and a straightforward indu tion, (s2 , s3 ) ∈
[(G0|after(s2 ) ∩ Tr ) ∪ A0 |after (s0 ) ]⋆ . Then (s2 , s3 ) ∈ Ext1 (s0 , s1 ). Furthermore
by Lemma 7, after(s2 ) ⊆ after(s0 ). Hen e (s2 , s3 ) ∈ [(G0|after(s2 ) ∩ Tr ) ∪
A0 |after (s2 ) ]⋆ . Therefore, by Proposition 1, (s2 , s3 ) ∈ Reach3 .
Due to Lemma 11, be ause

Claim 17. S′ ⊆ interfereG0∪A0 (S1 ).
Proof.

s ∈ S′ . Therefore there exists s0 ∈ S0 su h that (s0 , s) ∈ Reach
and label (s) = ℓ3 6= ℓ1 . A ording to Lemma 31 there exists s1 su h that
(s0 , s1 ) ∈ Reach1 , label (s1 ) = ℓ3 and s ∈ interfereG0 ∪A0 {s1 }. Therefore
s1 ∈ S1 and s ∈ interfere G0 ∪A0 (S1 ).
Let

Claim 18. Self ⊆ Self1 .
Proof.

(s, s′ ) ∈ Self. A ording to Lemma 1, label (s) 6= ℓ3 . There
exists s0 ∈ S0 su h that (s0 , s) ∈ Reach. Therefore, a ording to lemma
31, s ∈ interfere A0 {s0 }. Therefore (s0 , s) ∈ Reach1 and, by Lemma 13,
label(s) = ℓ1 . Due to Lemmas 2 and 28, (s, s′ ) ∈ Tr ℓ1 spawn(ℓ2 ),ℓ3 . Hen e
(s, s′ ) ∈ Self1 .
Let

Claim 19. Par ⊆ Self3 ∪ Par3 .
Proof.

(s, s′ ) ∈ Par. Therefore, there exists s0 ∈ S0 su h that (s0 , s) ∈
Reach; Schedule and s ∈ after (s0 ). Noti e that by denition of Schedule ,
thread (s0 ) 6= thread (s).
Assume by ontradi tion, that s ∈ Schedulehinterfere A0 {s0 }i. Due to
Lemma 11, thread (s0 ) = thread (s). This is ontradi tory.
Hen e, by Lemma 31, there exists s1 , s2 , s3 su h that (s0 , s1 ) ∈ Reach1 ,
(s1 , s2 ) ∈ Schedule , (s2 , s3 ) ∈ Reach3 , (s3 , s) ∈ Schedule , s2 ∈ s hedule- hild {s1 },
and label (s1 ) = label(s) = ℓ3 .
Hen e, s1 ∈ S1 , s2 ∈ S2 .
A ording to Lemma 8 after (s1 ) ∩ after (s2 ) = ∅. Given that (s2 , s) ∈
Reach; Schedule; Schedule , (s2 , s) ∈ (G0 ∪ A0 )⋆|after (s ) . Hen e, du to Lemma
1
26, s ∈ after(s2 ).
Let

3

G-COLLECTING SEMANTICS

36

thread (s) = thread (s2 ), then (s2 , s) ∈ Reach3
thread (s) 6= thread (s2 ), then (s, s′ ) ∈ Par3 .
If

and

(s, s′ ) ∈ Self3 .

If

Claim 20. Sub ⊆ Self3 ∪ Par3 .
Proof.

(s, s′ ) ∈ Sub. There exists s0 , s4 su h that (s0 , s4 ) ∈ Reach and
(s4 , s) ∈ Ext(s0 , s4 ) and s4 ∈ S′ . By Lemma 31, there exists s1 , s2 , s3 su h
that (s0 , s1 ) ∈ Reach1 , s2 ∈ s hedule- hild A ({s1 }), (s2 , s3 ) ∈ Reach3 ∩
Ext1 (s0 , s1 ) and (s3 , s4 ) ∈ Schedule .
Furthermore, s ∈ after(s0 ) r after(s4 ). Due to Lemma 29, either s ∈
after (s1 ) r after(s4 ) or s ∈ after (s2 ) r after(s4 ).
′
Assume by ontradi tion that s ∈ after (s1 )rafter (s4 ). Therefore (s, s ) ∈
Sub1 . But, by Claim 2, Sub1 = ∅. Therefore s ∈ after (s2 ) r after (s4 ).
Let (i, P, σ, g) = s and s5 = (thread (s2 ), P5 , σ5 , g5 ).
∗
Given that (s4 , s) ∈ Ext(s0 , s4 ), (s4 , s) ∈ [(G0|after (s0 ) ∩ Tr ) ∪ A2 |after (s ) ]
0
∗
and by Lemma 29, (s4 , s) ∈ [(G0|after(s1 )∪after (s2 ) ∩ Tr ) ∪ A2 |after(s ) ] .
0
By denition of post, after (s1 ) ⊆ post(ℓ2 ). Furthermore by Lemma 8,
after (s1 ) ∩ after(s2 ) = ∅. Therefore after (s1 ) ⊆ post(ℓ2 ) r after (s2 ). Hen e,
(s4 , s) ∈ [(G0 |after (s2 ) ∩ Tr ) ∪ A2 |after(s0 ) ∪ G0 |post(ℓ2 )rafter (s2 ) ]∗ . By Lemma 7,
after (s2 ) ⊆ after(s), therefore (s4 , s) ∈ [(G0|after(s2 ) ∩Tr )∪(A2 ∪G0|post(ℓ2 ) )|after (s0 ) ]∗ .
∗
By Proposition 1, (s4 , s) ∈ [(G∞|after(s2 ) ∩ Tr ) ∪ (A2 ∪ G0|post(ℓ2 ) )|after (s ) ] .
0
Let (i, P, σ, g) = s and s5 = (thread (s2 ), P, σ, g). Therefore, (s2 , s5 ) ∈
Reach3 .
′
If i = thread (s2 ), then s5 = s and (s, s ) ∈ Self3 . If i 6= thread (s2 ), then
(s5 , s) ∈ Schedule and (s, s′ ) ∈ Par3 .
Let

3.6 Overapproximation of the Exe ution of a Program
Lemma 32. For all P and σ, after ((main, P, σ, ǫ)) = States.

In parti ular, if Init is the set of initial states of a program and s ∈ Init ,
then after (s) = States.
The following proposition shows the
and the

G-

onne tion between the operational

olle ting semanti s.

Proposition 4

(Conne tion with the operational semanti s)

program cmd, ℓ∞ and its set of initial states Init . Let:
ℓ

def

hS′ , G′ , A′ i =

ℓ


cmd , ℓ∞ hInit, G∞ , Schedulei

. Consider a

4

ABSTRACT SEMANTICS

37

with G∞ = guarantee ℓ cmd,ℓ  hInit, Schedule, Schedulei
∞

Then:

S′ = {(main, P, σ, g) ∈ Tr ⋆ℓ cmd,ℓ∞ hIniti | P (main) = ℓ∞ }
G′ = G∞ = {(s, s′) ∈ Tr ℓ cmd,ℓ∞ | s ∈ Tr ⋆ℓ cmd,ℓ∞ hIniti} ∪ Schedule
A′ = {(s, s′) ∈ Tr ℓ cmd,ℓ∞ | s ∈ Tr ⋆ℓ cmd,ℓ∞ hIniti ∧ thread (s) 6= main}
∪Schedule

Proof. We only have to prove that Reach = {s ∈ Tr ⋆ℓ cmd,ℓ∞ hIniti | thread (s) =
main }.
s1 ∈ {s ∈ Tr ⋆ℓ cmd,ℓ∞ hIniti | thread (s) = main }.
⋆
There exists s0 ∈ S su h that (s0 , s) ∈ Tr ℓ cmd,ℓ By proposition 1, (s0 , s) ∈
∞
G∞ ∩ Tr ⋆ℓ cmd,ℓ∞
⋆
By Lemma 32, (s0 , s)(G∞|after (s0 ) ∩ Tr ℓ cmd,ℓ ) ∪ Schedule |after(s ) . Hen e
∞
0
(s0 , s).
⋆
It is straightforward to he k that Reach ⊆ {s ∈ Tr ℓ cmd,ℓ hIniti | thread (s) =
∞
main }.

Proof.

Let

⋆
Re all that Tr ℓ cmd,ℓ (Init) is the set of states that o ur on paths starting
∞
′
from Init . S represents all nal states rea hable by the whole program from
′
an initial state. G represents all transitions that may be done during any
′
exe ution of the program and A represents transitions of hildren of
.

main

4

Abstra t Semanti s

4.1 Abstra tion
Re all from the theory of abstra t interpretation [4℄ that a

Galois on-

ne tion

[23℄ between a

It is a

lassi al result [23℄ that an adjoint uniquely determines the other in

X and an abstra t omplete
latti e Y is a pair of monotoni fun tions α : X → Y and γ : Y → X su h
that ∀x ∈ X, ∀y ∈ Y, α(x) 6 y ⇔ x 6 γ(y); α is alled the abstra tion fun tion and γ the on retization fun tion. Produ t latti es are ordered by the
produ t ordering and sets of fun tions from X to a latti e L are ordered by
the pointwise ordering f 6 g ⇔ ∀x ∈ X, f (x) 6 g(x). A monotoni fun tion
f ♯ is an abstra tion of a monotoni fun tion f ♭ if and only if α ◦ f ♭ ◦ γ 6 f ♯ .
a Galois

on rete

omplete latti e

onne tion; therefore, we sometimes omit the abstra tion fun tion

(lower adjoint) or the

on retization fun tion (upper adjoint).

4

ABSTRACT SEMANTICS

Our

38

on rete latti es are the powersets

P(States) and P(Tr) ordered

by

in lusion. Remember, our goal is to adapt any given single-thread analysis
in a multithreaded setting. A
latti e

D

ordingly, we are given an abstra t

of abstra t states and an abstra t

transitions.

These

omplete latti e

R

omplete

of abstra t

on rete and abstra t latti es are linked by two Galois

αD , γD

onne tions, respe tively

and

αR , γR.

We assume that abstra tions

of states and transitions depend only on stores and that all the transitions
that leave the store un hanged are in
abstra t

guard

and

spawn

of Table 1, whi h are

or-

re t abstra tion of the

or-

responding on rete fun tions.

ℓ⋆ ∈ Labels

⊥.

Con rete fun tion

given the abstra t operators

a

spe ial label whi h is never
used in statements. Furtherdef
more, we dene post(ℓ⋆ ) =

States.
We dene a Galois

This assumption allows us to

as the least abstra t transition

We also assume we are

We assume

γR (⊥).

on-

Abstra t fun tion

λ(i, P, σ, g).(i, P, write lv:=e (σ), g)
w rite lv:=e
:
D →D
λA, S.interfereA (S)
inter : R × D →
D
λS.{(i, P, σ, g), (i, P ′ , σ ′ , g′ ) ∈ w rite -inter lv:=e :
Tr|
(i, P, σ, g) ∈ S ∧ σ ′ ∈ D → R
write lv:=e (S)}
λS.{(i, P, σ, h)
∈
S
| enforce cond
:
bool (σ, cond ) = true}
D →D

P(States)
and P(Labels): αL (S) = {ℓ ∈
Table 1: Given abstra tions
Labels | S ∩ post
(ℓ)
=
6
∅}
T
and γL (L ) =
ℓ∈LabelsrL post(ℓ) (by onvention, this set is States when
L = Labels). The set αL (S) represents the set of labels that may have been

ne tion between

en ountered before rea hing this point of the program.

Note that we have two distin t ways of abstra ting states
by using

αD ,

whi h only depends on the store

depends on the genealogy
to the multithreaded

g

and the

σ,

(i, P, σ, g), either
αL whi h only

or by using

urrent thread

i.

The latter is spe i

ase, and is used to infer information about possible

interferen es.
Just as

αR

αD

was not enough to abstra t states in the multithreaded setting,

is not enough, and lose the information that a given transition is or not

in a given

post(ℓ).

This information is needed be ause

Theorem 1 and Fig. 7.

G|post(ℓ)

Let us introdu e the following Galois

is used in
onne tion

P(Tr) and the abstra t latti e R Labels, the
produ t of |Labels| opies of P(Tr), to this end: αK (G) = λℓ.αR (G|post(ℓ) )
γK (K ) = {(s, s′) ∈ Tr | ∀ℓ ∈ Labels, s ∈ post(ℓ) ⇒ (s, s′ ) ∈ γR (K (ℓ))}.

between the

on rete latti e

4

ABSTRACT SEMANTICS

K = αK (G)

39

is an abstra tion of the guarantee

ondition:

K (ℓ⋆ )

represents

K (ℓ) represents the interferen es of a hild with its
G|post(ℓ) .
Abstra t ongurations are tuples hC , L , K , I i ∈ D×P(Labels)×R Labels ×
R su h that inter I C = C and ℓ⋆ ∈ L . The meaning of ea h omponent of an
abstra t onguration is given by the Galois onne tion α fg , γ fg :
the whole set

G,

and

parent, i.e., abstra ts

def

α fg hS, G, Ai = hinter αR (A) (αD (S)), αL (S), αK (G), αR (A)i
def

γ fg hS, G, Ai = hγD (C ) ∩ γL (L ), γK (K ), γR (I )i
C

abstra ts the possible

so far in the exe ution.

urrent stores

I

S. L

abstra ts the labels en ountered

is an abstra tion of interferen es

A.

4.2 Appli ations: Non-Relational Stores and Gen/Kill
Analyses
As an appli ation, we show some

on rete and abstra t stores that

used in pra ti e. We dene a Galois onne tion
and abstra t stores and en ode both
as abstra t stores, i.e.,

D = R.

αstore , γstore between

abstra t states

Abstra t states are

and

an be
on rete

abstra t transitions

on retized by:

def

γD (σ ♯ ) = {(i, P, σ, g) | σ ∈ γstore (σ ♯ )}.

Non-relational store

Su h a store is a map from the set of variables

on rete values
abstra t values

♭

Var
Var

V of
, and abstra t stores are maps from
♯
omplete latti e V of
. Given a Galois onne tion
♭
♯
between V and V , the following is a lassi al, so alled non-relational

to some set
to some

αV , γV

abstra tion of stores:

def

αstore (σ) = λx.αD (σ(x))
Let

val C (e)

and

addr C (lv)

and

def

γstore (σ ♯ ) = {σ | ∀x, σ(x) ∈ γD (x)}.

be the abstra t value of the expression

the set of variables that may be represented by

lv , respe

tively, in the

e

and

ontext

4

ABSTRACT SEMANTICS

40

C.
def

γR (σ ♯ ) =

def


((i, P, σ, h), (i′ , P ′ , σ ′ , h′ )) | ∀x, σ ′ (x) ∈ γD (σ ♯ (x)) ∪ {σ(x)}

w rite x:=e (C ) = C [x 7→ val C (e)]
[
def
w rite x:=e (C )
w rite lv:=e (C ) =
x∈addr C (lv)

def

w rite -inter lv:=e (C ) = λx.if x ∈ addr C (lv)

then

val C (e)

else

⊥

def

inter I (C ) = I ⊔ C
def

enforce x (σ) = σ[x 7→ true ♯ ]

Gen/kill analyses

and

enforce ¬x (σ) = σ[x 7→ false ♯ ]

In su h analyses [6℄, stores are sets, e.g., sets of ini-

tialized variables, sets of edges of a point-to graph.

The set of stores is

P(X) for some set X , D = R = P(X), and the abstra tion is trivial
αstore = γstore = id . Ea h gen/kill analysis gives, for ea h assignment, two
sets: gen(lv := e, σ) and kill(lv := e, σ). These sets may take the urrent
store σ into a ount (e.g. Rugina and Rinard's strong ag [12, 13℄); gen
(resp. kill ) is monotoni (resp. de reasing) in σ . We dene the on retization
of transitions and the abstra t operators:

def

γR (σ ♯ ) =

def


(i, P, σ, h) → (i′ , P ′, σ ′ , h′ ) | σ ′ ⊆ σ ∪ σ ♯

w rite lv:=e (C ) = (C r kill (lv := e, σ)) ∪ gen(lv := e, σ)
def

w rite -inter lv:=e (C ) = gen(lv := e, σ)
def

inter I (C ) = I ∪ C
def

enforce x (σ) = σ

4.3 Semanti s of Commands
Lemma 33. αL (S) = αL (interfereA (S)).
Lemma 34. αL (s hedule- hild (S)) = λℓ.⊥.
Lemma 35. Let G1 and G2 two set of transitions and S2 = {s | ∃s′ : (s, s′ ) ∈

G2 }.

Hen e, αK (G1 ∪G2 ) 6 λℓ.if ℓ ∈ αL (S2 ) then K (ℓ)⊔w rite -inter lv:=e (C ) else K (ℓ)

4

ABSTRACT SEMANTICS

assign lv:=e hC , L , K , I i
′′
with K
= λℓ.if ℓ ∈ L then
guard cond hC , L , K , I i
spaw n ℓ hC , L , K , I i
child -spaw n ℓ hC , L , K , I i
com bine hC ,L ,K ,I i (K ′ )
execute -thread ℓ cmd,ℓ′ ,C ,L ,I (K )
′
′
′ ′
with hC , L , K , I i
guarantee ℓ cmd,ℓ′ (hC , L , K , I i)

41

def

= hinter I ◦ w rite lv:=e (C ), L , K ′′ , I i
K (ℓ) ⊔ w rite -inter lv:=e (C ) else K (ℓ)
def
= hinter I ◦ enforce cond (C ), L , K , I i
def
= hC , L ∪ {ℓ}, K , I i
def
= hinter I ⊔K (ℓ) (C ), L , λℓ.⊥, I ⊔ K (ℓ)i
def
= hinter I ⊔K ′ (ℓ⋆ ) (C ), L , K ⊔ K ′ , I ⊔ K ′ (ℓ⋆ )i
def
= K′
= Lℓ cmd, ℓ′ MhC , L , K , I i
def
= execute -thread ↑ω
ℓ cmd,ℓ′ ,C ,L ,I (K )

Figure 8: Basi

abstra t semanti

The fun tions of Fig. 8 abstra t the

fun tions

orresponding fun tions of the

G-

olle ting semanti s (See Fig. 7).

Proposition 5. The abstra t fun tions assign lv:=e , guard cond , spaw n ℓ2 , child
-spaw n ℓ2 ,


ℓ
com bine
 ℓ abstra tionsof the on rete fun
  ℓand guarantee ℓ cmd
 are
 ℓ tions lv :=

′
′
e, ℓ , guard(cond), ℓ , 1 spawn(ℓ2 ), ℓ3 , init- hild ℓ1 ◦ 1 spawn(ℓ2 ), ℓ3 ,
 respe tively.
ombine and guarantee ℓ
cmd ,ℓ∞

Proof.

are straightforward. The ase
The ases of com bine and guarantee ℓ
cmd
child -spaw n ℓ2 is a straightforward onsequen e of Lemma 34.
Let hC , L , K , I i an abstra t onguration and hS, G, Ai = γ fg hC , L , K , I i.
Therefore S = interfere A (S).
ℓ

′ ′ ′
Let hS , G , A i =
lv := e, ℓ′ and hC ′ , L ′ , K ′ , I ′ i = assign lv:=e hC , L , K , I i.
Therefore, by denition, inter I ◦ w rite ℓ lv:=e,ℓ′ ◦ inter I . By Proposition 2,

S′ = interfereA Tr ℓ lv:=e,ℓ′ r SchedulehinterfereA (S)i . Hen e αD (S′ ) 6 C ′ .
′
′
A ording to Proposition 2, G ⊆ G∪Gnew with Gnew = {(s, s ) ∈ Tr ℓ1 basic,ℓ2 |
′
s ∈ interfereA (S)} = {(s, s ) ∈ Tr ℓ1 basic,ℓ2 | s ∈ S}. Hen e αR (Gnew ) 6
w rite -inter ℓ lv:=e,ℓ′ (C ).

of

Therefore by Lemma 35:

αK (G′ ) 6 λℓ.if ℓ ∈ L then K (ℓ) ⊔ w rite -inter lv:=e (C ) else K (ℓ)
′
′
If (s, s ) ∈ Tr ℓ lv:=e,ℓ′ then, s ∈ post(ℓ) ⇔ s ∈ post(ℓ). Therefore, by
′
Lemma 33, αL (S) = αL (S ).
′ ′ ′
′
′
′ ′
Hen e α fg (hS , G , A i) 6 hC , L , K , I i. Given that αR (Tr ℓ guard (cond ),ℓ′ ) =
⊥ and ∀(s, s′ ) ∈ Tr ℓ guard(cond ),ℓ′ , s′ ∈ post(ℓ) ⇔
 ℓ s ∈ post(ℓ), we
 prove in the
′
guard(cond), ℓ .
is an abstra tion of
same way that guard
cond

4

ABSTRACT SEMANTICS

Lℓ lv := eMQ
Lℓ1 cmd 1 ; ℓ2 cmd 2 MQ
Lℓ1 while(cond){ℓ2 cmd}MQ
′
with loop (Q )
Lℓ1 create(ℓ2 cmd)MQ
′
with Q

def

=
=
def
=
def
=
def
=
def
=
def

42

assign lv:=e Q
Lℓ2 cmd 2 M ◦ Lℓ1 cmd 1 MQ
guard ¬cond loop ↑ω Q

LcmdM ◦ guard cond Q ′ ⊔ Q ′
com bine Q ′ ◦ guarantee ↑ω
ℓ2 cmd ◦ child -spaw n ℓ (Q )
2
spaw n ℓ2 (Q )

Figure 9: Abstra t semanti s

αR (Tr ℓ1 spawn(ℓ2 ),ℓ3 ) = ⊥ and ∀(s, s′ ) ∈ Tr ℓ1 spawn(ℓ2 ),ℓ3 , s′ ∈ post(ℓ) ⇔
s ∈ post(ℓ) ∨ ℓ = ℓ2 , we prove in the same way thatspaw n ℓ2 is an abstra tion

ℓ
of 1 spawn(ℓ2 ), ℓ3 .
Given that

The assign
fun tion updates K by adding the modi ation of the store
lv:=e
to all labels en ountered so far (those whi h are in L ). It does not hange

L

be ause no thread is

store, we

reated. Noti e that in the

an simplify fun tion

assign

ase of a non-relational

using the fa t that

inter I ◦ w rite x:=e (C ) =

C [x 7→ val C (e) ⊔ I (x)].
The abstra t semanti s is dened by indu tion on syntax, see Fig. 9, and,
with Prop.5, it is straightforward to

he k the soundness of this semanti s:

Theorem 2 (Soundness). Lcmd, ℓM is an abstra tion of cmd, ℓ .




4.4 Example
Consider Fig. 10 and the non-relational store of ranges [4℄.

We will apply

our algorithm on this example.
Our algorithm

omputes a rst time

not rea hed, and then,

is

then, the xpoint is

omputed another time.

Q 0 = hC 0 , {ℓ⋆ }, K 0, ⊥i where C 0 = [y =?, z =?]
and L 0 = {ℓ⋆ } and K 0 = λℓ.⊥ and I 0 = ⊥.
ℓ

1
The onguration Q 1 =
y := 0; ℓ2 z := 0, ℓ3 (Q 0 ) is omputed. Q 1 =
hC 1 , {ℓ⋆ }, K 1, ⊥i where C 1 = [y = 0, z = 0] and K 1 = ℓ⋆ 7→ [y = 0, z =
0]. The L and I omponnents are not hanged be ause no new thread

1. Initial

2.

execute -thread

execute -thread ,

is

onguration :

reated.

4

ABSTRACT SEMANTICS

43

Q 2 = child -spaw n ℓ3 (Q 1 ) is omputed. Q 2 = hC 2 , {ℓ⋆ }, K 2, ⊥i
where C 2 = C 1 and K 2 = λℓ.⊥. Noti e that be ause K 1 (ℓ3 ) = ⊥ the
equality C 2 = C 1 holds.
ℓ

4
The onguration Q 3 =
y := y + z, ℓ∞ (Q 2 ) is omputed. Q 3 =
hC 3 , {ℓ⋆ }, K 3, ⊥i where C 3 = [y = 0, z = 0] and K 3 = ℓ⋆ 7→ [y = 0].

3. The onguration

4.

Q 4 = com bine spaw n ℓ (Q 2 ) (Q 3 ) is omputed. Q 4 = hC 4 , {ℓ⋆ , ℓ3 }, K 4, I 4 i.
3
C 4 = [y = 0, z = 0] and K 4 = [ℓ⋆ 7→ [y = 0, z = 0]] and I 4 = [y = 0].

ℓ
5
The onguration Q 5 =
z := 3, ℓ∞ Q 4 is omputed. Q 5 = hC 5 , {ℓ⋆ , ℓ3 }, K 5 , I 5 i.
C 5 = [y = 0, z = 3] and K 5 = [ℓ⋆ 7→ [y = 0, z = [0, 3]] and I 5 = I 4 .

5. The onguration

6.

Then, we
ration

ompute a se ond time

execute -thread ,

on a new initial

ongu-

hC 0 , L 0 , K 5 , I 0 i.

Noting hange, ex ept at the step 3, when

child -spaw n
′
is applied. The onguration obtained is then Q 2 =
hC 2′ , {ℓ⋆ }, K 5, I 2′ i where C 2′ = [y = 0, z = [0, 3]] and
I 2′ = [z = 3]. Then, the algorithm dis overs that the
value of y may be 3.
The details of the exe ution of the algorithm is
given in the following tabular:

ℓ1

y := 0; ℓ2 z := 0;
ℓ3
create(ℓ4 y := y + z);
ℓ5
z := 3, ℓ∞

Figure 10:
ple

Exam-

5

PRACTICAL RESULTS

Initial

ℓ

onguration

1

y := 0, ℓ2

ℓ

2

z := 0, ℓ3

ℓ

4





child -spaw n ℓ3

y := y + z, ℓ∞

com bine spaw n ℓ

3

ℓ

5

ℓ

1

y := 0, ℓ2

ℓ

2

z := 0, ℓ3

ℓ

4

(·)

z := 3, ℓ∞

Initial





onguration





child -spaw n ℓ3

y := y + z, ℓ∞

com bine spaw n ℓ
ℓ

5

5

3

(·)

z := 3, ℓ∞





44

C
y = ?
z = ?
y = 0
z = ?
y = 0
z = 0
y = 0
z = 0
y = 0
z = 0
y = 0
z = 0
y = 0
z = 3
y = ?
z = ?
y = 0
z = ?
y = 0
z = 0
y =
0
z = [0, 3]
y = [0, 3]
z = [0, 3]
y = [0, 3]
z =
0
y = [0, 3]
z =
3

L

K

I

{ℓ⋆ }

λℓ.⊥

⊥

{ℓ⋆ }

ℓ⋆ 7→ y = 0

⊥

{ℓ⋆ }

ℓ⋆ 7→ y = 0, z = 0

⊥

{ℓ⋆ }

λℓ.⊥

⊥

{ℓ⋆ }

ℓ⋆ 7→ y = 0

⊥

{ℓ⋆ , ℓ3 }

ℓ⋆ 7→ y = 0, z = 0

y=0

ℓ⋆
ℓ3
ℓ⋆
ℓ3
ℓ⋆
ℓ3
ℓ⋆
ℓ3

{ℓ⋆ , ℓ3 }
{ℓ⋆ }
{ℓ⋆ }
{ℓ⋆ }

7→
7→
7
→
7→
7
→
7→
7
→
7→

y = 0, z = [0, 3]
z=3
y = 0, z = [0, 3]
z=3
y = 0, z = [0, 3]
z=3
y = 0, z = [0, 3]
z=3

⊥
z=3

{ℓ⋆ }

ℓ⋆ 7→ y = [0, 3]

z=3

{ℓ⋆ , ℓ3 }
{ℓ⋆ , ℓ3 }

ℓ⋆
ℓ3
ℓ⋆
ℓ3

7→ y = [0, 3], z = [0, 3]
7→
z=3
7
→
y = [0, 3], z = [0, 3]
7→
z=3

ompute it re ursively.

This requires to

ompute xpoints and may fail to terminate. For this rea↑ω
son, ea h time we have to ompute f (X) we ompute instead the over↑▽
approximation f , where ▽ is a widening operator, in the following way:
2. Compute

⊥

λℓ.⊥

The abstra t semanti s is denotational, so we may

X1 := X

⊥

{ℓ⋆ }

Pra ti al Results

1. Assign

y=0

X2 := f (X1 )

3. If

X2 6 X 1

then returns

X2 ,

y = [0, 3]
y = [0, 3]

5

PRACTICAL RESULTS

45

X1 := X1 ▽X2 and go ba k to 2. Our nal algorithm
is to ompute re ursively guarantee ℓ
applied to the initial onguration
cmd,ℓ∞
h⊤, {ℓ⋆ }, λℓ.⊥, ⊥i, overapproximating all xpoint omputations.
otherwise, 4. Assign

We have implemented

L.o.C.

two tools, Parint and MT-

two dierent abstra t stores.
The rst one maps variables to integer intervals
and

omputes an over-

false

time

65

0.05

0.20s

0

27 100

-

0.34s

7

Message
Embedded

MT-Penjili

time

Penjili, in O aml with the
front-end C2newspeak, with

Parint

alarms

Test 12

342

-

3.7s

1

Test 15

414

3.8

-

-

approximation of the val-

Table 2: Ben hmarks

ues of the variables. The

se ond one extends the analysis of Allamigeon et al. [2℄, whi h fo uses on
pointers, integers, C-style strings and stru ts and dete ts array overows.
It analyzes programs in full edged C (ex ept for dynami

memory allo a-

tion library routines) that use the Pthreads multithread library. We ignore
mutexes and

ondition variables in these implementations. This is sound be-

ause mutexes and

ondition variables only restri t possible transitions. We

lose pre ision if mutexes are used to

reate atomi

blo ks, but not if they are

used only to prevent data-ra es.
In Table 2 we show some results on ben hmarks of dierents sizes. L.o.C.
means Lines of Code.

Message is a C le, with 3 threads: one thread

sends an integer message to another through a shared variable. Embedded
is extra ted from embedded C

ode with two threads. Test 12 and Test

15 are sets of 12 and 15 les respe tively, ea h one fo using on a spe i
thread intera tion.
To give an idea of the pre ision of the analysis, we indi ate how many
false alarms were raised. Our preliminary experiments show that our algorithm loses pre ision in two ways: 1. through the (single-thread) abstra tion
on stores 2. by abstra tion on interferen es. Indeed, even though our algorithm takes the order of transitions into a

ount for the

urrent thread, it

onsiders that interferen e transitions may be exe uted in an arbitrary order
and arbitrary many times. This does not

ause any loss in Message, sin e

the thread whi h send the message never put an in orre t value in the shared
variable. Despite the fa t that Embedded is a large ex erpt of an a tual
industrial

ode, the loss of pre ision is moderate: 7 false alarms are reported

6

COMPLEXITY

46

on a total of 27 100 lines. Furthermore, be ause of this arbitrary order, our
analysis straightforwardly extends to models with "relaxed- onsisten y" and
"temporary" view of thread memory due to the use of

a he, e.g., OpenMP.

6

Complexity

The

omplexity of our algorithm greatly depends on widening and narrowing
ℓ
Given a program 0 prog, ℓ∞ , the
of the widening and

slowness

operators.

narrowing in an integer
at most

w

w

su h that: widening-narrowing stops in always

steps on ea h loop and whenever

guarantee

is

omputed (whi h

also requires doing an abstra t xpoint

omputation). Let the

of a program be the nesting depth of

while

sub ommand

and of

create

nesting depth

whi h

2

have a

create .

Proposition 6. Let d be the nesting depth, n the number of ommands of

our program, and, w the slowless of our widening. The time omplexity of
our analysis is O(nw d+1) assuming operations on abstra t stores are done in
onstant time.
This is

omparable to the

thread analysis, and

O(nw d )

omplexity of the

ertainly mu h better that the

orresponding single-

ombinatorial explosion

of interleaving-based analyses. Furthermore, this is beter than polynomial in
an exponential number of states [15℄.

Proof.

c(ℓ cmd, ℓ′ ), n(ℓ cmd , ℓ′) and d(ℓ cmd , ℓ′ ) and w(ℓ cmd , ℓ′ ) be the
ℓ
′
ℓ
′
omplexity of analyzing cmd , ℓ , the size of cmd , ℓ and the nesting depth of
ℓ
′
cmd, ℓ , the slowless of the widening and narrowing on ℓ cmd , ℓ′ respe tively.
Let a and k the omplexity of assign and of reading K (ℓ) respe tively.
Let

Proposition 6 is a straightforward

3

onsequen e of the following lemma :

Lemma 36. The omplexity of omputing Lℓ cmd, ℓ′ MQ is O(an(w + k)wd−1 )
This lemma is proven by indu tion.

c(lv := e) = a
c(ℓ1 cmd 1 ; ℓ2 cmd 2 , ℓ3 ) = c(ℓ1 cmd 1 , ℓ2 ) + c(ℓ2 cmd 2 , ℓ3 )
2 In

our Semanti s, ea h create needs a xpoint omputation, ex ept create with no
sub ommand create .
3 The fun tions arguments are omitted in the name of simpli ity.

6

COMPLEXITY

47

c(ℓ1 while(cond){ℓ2 cmd}, ℓ3 ) 6 w(ℓ1 while(cond ){ℓ2 cmd }, ℓ3 ) × c(ℓ2 cmd , ℓ1 )
ℓ2

cmd

ontain any sub ommand create , then the xpoint
ℓ
ℓ
ℓ
omputation terminates in one step: c( 1 create( 2 cmd ), ℓ3 ) = k + c( 2 cmd )
ℓ1
ℓ2
ℓ1
ℓ2
ℓ2
Else: c( create( cmd ), ℓ3 ) = k + w( create( cmd ), ℓ3 )) × c( cmd)
If

does not

6.1 Complexity of Operations on R Labels
Noti e that we have assumed that operation on
stant time in Proposition 6.
dierent ways.

R Labels

are done in

on-

This abstra t store may be represented in

The main problem is the

omplexity of the

assign

fun -

tion, whi h

omputes a union for ea h element in L . The naive approa h
Labels
is to represent K ∈ R
as a map from P(Labels) to R . Assuming

that operations on maps are done in onstant time, this approa h yields
O(tnw d ) omplexity where t is the number4 of create s in the program.
Labels
We may also represent K ∈ R
as some map K M from P(Labels)
a

S
K (ℓ) = L ∋ℓ K M (L ) and the fun tion assign is done in
def
hC , L , K , I i = hinter I ◦ w rite lv:=e (C ), L , K M [L 7→
onstant time : assign
lv:=e
K M (L ) ⊔ w rite -inter lv:=e (C )], I i. Nevertheless, to a ess to the value K (ℓ)
may need up to t operations, whi h in reases the omplexity of child -spaw n
d−1
and com bine . The omplexity is then O(n(w + t)w
).
to

R

su h that

6.2 Compexity of Widdenning
The slowness of the widening and narrowing operators,

w,

depends on the

abstra tion. Nevertheless, a widening is supposed to be fast.
′
′
Consider the naive widening on intervals : [x, x ]▽[y, y ] =

(
x
z=
−∞

if

y>x

else

and

(
x′
z′ =
+∞

if

y6x

else

[z ′ , z ′ ]

where

.

This widening never widen more than two times on the same variable. Therefore this naive widening is linear in the worst
4 This

ase.

is dierent to the number of threads sin e an arbitrary number of threads may
be reated at the same lo ation.

7

CONCLUSION

48

def

Lℓ0 par {ℓ1 cmd 1 |ℓ2 cmd 2 }M(Q ) = hC 1 ⊓ C 2 , L , K ′ , I 1 ⊔ I 2 i
with hC 1 , L 1 , K 1 , I 1 i = guarantee ℓ1
◦ child -spaw n ℓ1 (Q )
cmd 1 ,ℓ∞
and hC 2 , L 2 , K 2 , I 2 i = guarantee ℓ2
◦ child -spaw n ℓ2 (Q )
cmd 2 ,ℓ∞
′
and K = K [ℓ1 7→ K 2 (ℓ⋆ ) ⊔ K (ℓ1 )][ℓ2 7→ K 1 (ℓ⋆ ) ⊔ K (ℓ2 )]
Figure 11: Extended syntax

6.3 Other form of parallelism
Our te hnique also applies to other forms of
how Rugina and Rinard's

par

on urren y, Fig. 11 displays

onstru tor [12, 13℄ would be

omputed with

our abstra tion. Corre tness is a straightforward extension of the te hniques
des ribed in this paper.
Our model handle programs that use

create

OpenMP programs with parallel and task

7

and

par .

Then, it

an handle

onstru tors.

Con lusion

We have des ribed a generi

stati

analysis te hnique for multithreaded pro-

grams parametrized by a single-thread analysis framework and based on a
form of rely-guarantee reasoning.

modular

To our knowledge, this is the rst su h

framework: all previous analysis frameworks

ti ular abstra t domain.

on entrated on a par-

Su h modularity allows us to leverage any stati

analysis te hnique to the multithreaded

ase.

We have illustrated this by

applying it to two abstra t domains: an interval based one, and a ri her
one that also analyzes array overows, strings, pointers [2℄. Both have been
implemented.
We have shown that our framework only in urred a moderate (low-degree
polynomial) amount of added

omplexity. In parti ular, we avoid the

om-

binatorial explosion of all interleaving based approa hes.
Our analyses are always

orre t, and produ e reasonably pre ise infor-

mation on the programs we tested.
lo ks/mutexes and

onditions into a

lieve that is an orthogonal
is already present
from the

without

on ern:

Clearly, for some programs, taking
ount will improve pre ision.

We be-

the non-trivial part of our te hnique

syn hronization primitives, as should be manifest

orre tness proof of our

G-

olle ting semanti s.

We leave the in-

8

ACKNOWLEDGMENT

49

tegration of syn hronisation primitives with our te hnique as future work.
However, lo ks whose sole purpose are to prevent data ra es (e.g. ensuring
that two

on urrent a

esses to the same variable are done in some arbitrary

sequential order) have no inuen e on pre ision. Taking lo ks into a
may be interesting to isolate atomi

8

ount

blo ks.

A knowledgment

We thank Jean Goubault-Larre q for helpful

omments.

Referen es
[1℄ A. Miné, Field-sensitive value analysis of embedded C programs with
union types and pointer arithmeti s, in: ACM SIGPLAN LCTES'06,
ACM Press, 2006, pp. 5463,

arti le-mine-l tes06.pdf.

http://www.di.ens.fr/~mine/publi/

[2℄ X. Allamigeon, W. Godard, C. Hymans, Stati

Analysis of String Ma-

nipulations in Criti al Embedded C Programs, in: K. Yi (Ed.), Stati
Analysis, 13th International Symposium (SAS'06), Vol. 4134 of Le ture
Notes in Computer S ien e, Springer Verlag, Seoul, Korea, 2006, pp.
3551.
[3℄ B. Steensgaard, Points-to analysis in almost linear time, in: POPL '96:
Pro eedings of the 23rd ACM SIGPLAN-SIGACT symposium on Priniples of programming languages, ACM Press, New York, NY, USA,
1996, pp. 3241. doi:http://doi.a m.org/10.1145/237721.237727.
[4℄ P. Cousot, R. Cousot, Basi Con epts of Abstra t Interpretation, Kluwer
A ademi

Publishers.

[5℄ A. Miné,
bound
Verlag,

A new

matri es,
2001,

pp.

numeri al abstra t
in:

PADO

155172,

arti le-mine-padoII.pdf.

II,

domain based

Vol.

2053

of

on dieren e-

LNCS,

Springer-

http://www.di.ens.fr/~mine/publi/

[6℄ P. Lammi h, M. Müller-Olm, Pre ise xpoint-based analysis of programs
with thread- reation and pro edures, in: L. Caires, V. T. Vas on elos

REFERENCES

50

(Eds.), CONCUR, Vol. 4703 of Le ture Notes in Computer S ien e,
Springer, 2007, pp. 287302.
[7℄ P. Pratikakis, J. S. Foster, M. Hi ks, Lo ksmith:

ontext-sensitive

or-

relation analysis for ra e dete tion, in: PLDI '06: Pro eedings of the
2006 ACM SIGPLAN

onferen e on Programming language design and

implementation, ACM Press, New York, NY, USA, 2006, pp. 320331.
doi:http://doi.a m.org/10.1145/1133981.1134019.
[8℄ L. Fajstrup, E. Goubault, M. Rauÿen, Dete ting deadlo ks in

on urrent

systems, in: CONCUR '98: Pro eedings of the 9th International Conferen e on Con urren y Theory, Springer-Verlag, London, UK, 1998, pp.
332347.
[9℄ D. R. Butenhof, Programming with POSIX Threads, Addison-Wesley,
2006.
[10℄ P. Cousot, R. Cousot, Abstra t interpretation and appli ation to logi
programs, Journal of Logi

Programming '92.

[11℄ L. O. Andersen, Program analysis and spe ialization for the C programming language, Ph.D. thesis, DIKU, University of Copenhagen
(May 1994).

http://repository.reads heme.org/ftp/papers/topps/
D-203.ps.gz
URL

[12℄ R. Rugina, M. C. Rinard, Pointer analysis for multithreaded programs,
in: PLDI, 1999, pp. 7790.
URL

iteseer.ist.psu.edu/rugina99pointer.html

[13℄ R. Rugina,

M. C. Rinard,

Pointer analysis for stru tured parallel

programs, ACM Trans. Program. Lang. Syst. 25 (1) (2003) 70116.
doi:http://doi.a m.org/10.1145/596980.596982.
[14℄ A. Venet, G. Brat, Pre ise and e ient stati

array bound

he king for

large embedded C programs, in: PLDI '04: Pro eedings of the ACM
SIGPLAN 2004

onferen e on Programming language design and im-

plementation, ACM Press, New York, NY, USA, 2004, pp. 231242.
doi:http://doi.a m.org/10.1145/996841.996869.

REFERENCES

51

[15℄ C. Flanagan, S. Qadeer, Thread-modular model

he king, in: T. Ball,

S. K. Rajamani (Eds.), SPIN, Vol. 2648 of Le ture Notes in Computer
S ien e, Springer, 2003, pp. 213224.
[16℄ A. Malkis, A. Podelski, A. Rybal henko, Pre ise thread-modular veri ation, in: H. R. Nielson, G. Filé (Eds.), SAS, Vol. 4634 of Le ture
Notes in Computer S ien e, Springer, 2007, pp. 218232.
[17℄ E. Yahav,
using

Verifying safety properties of

3-valued

logi ,

in:

POPL

'01:

on urrent java programs
Pro eedings

of

the

28th

ACM SIGPLAN-SIGACT symposium on Prin iples of programming
languages,

ACM

Press,

New

York,

NY,

USA,

2001,

pp.

2740.

doi:http://doi.a m.org/10.1145/360204.360206.
[18℄ T. W. Reps, Personnal

ommuni ation (2008).

[19℄ C. Flanagan, S. N. Freund, M. Lifshin, Type inferen e for atomi ity, in:
TLDI '05, ACM Press, 2005, pp. 4758.
[20℄ R. J. Lipton, Redu tion:

a method of proving properties of parallel

programs, Commun. ACM 18 (12) (1975) 717721.
[21℄ V. Vojdani, V. Vene, Goblint:

Path-sensitive data ra e analysis, in:

SPLST, 2007.
[22℄ V. Vene, M. Muller-olm, Global invariants for analyzing multi-threaded
appli ations, in: In Pro . of Estonian A ademy of S ien es: Phys., Math,
2003, pp. 413436.
[23℄ G. Gierz, K. Hofmann, K. Keimel, J. Lawson, M. Mislove, D. S ott,
Continuous Latti es and Domains, Cambridge University Press, 2003.

