We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). The concurrent program to be synthesized is specified by providing both the behavioural and the structural properties it should satisfy. Behavioural properties, such as safety and liveness properties, are specified by using formulas of the Computation Tree Logic, which are encoded as a logic program. Structural properties, such as the symmetry of processes, are also encoded as a logic program. Then, the program which is the union of these two encodings, is given as input to an ASP system which returns as output a set of answer sets. Finally, each answer set is decoded into a synthesized program that, by construction, satisfies the desired behavioural and structural properties.
We consider concurrent programs consisting of finite sets of processes which interact with each other through communication protocols. Such protocols are based on a set of instructions, called synchronization instructions, operating on shared variables ranging over finite domains. The communication protocols are realized in a distributed manner, that is, every process includes one or more regions of code consisting of synchronization instructions, responsible for the interaction between processes.
Even for a small number of processes, communication protocols which guarantee a desired behaviour of the concurrent programs may be hard to design. In this paper we propose a method for automatically synthesizing correct concurrent programs starting from the formal specification of their desired behaviour.
Methods for the automatic synthesis of concurrent programs from temporal
logic specifications have been proposed in the past by Clarke and Emerson [
We introduce a framework, based on logic programming, for the automatic
synthesis of concurrent programs. We assume that the behavioural properties of
the concurrent programs, such as safety and liveness properties, are specified
by using formulas of the Computation Tree Logic (CTL for short), which is a
very popular propositional temporal logic over branching time structures (see, for
instance, [
We show that every answer set (that is, every stable model) of the program Π
represents a concurrent program satisfying the given specification. Thus, by using
an Answer Set Programming (ASP) system, such as DLV [
We have performed some synthesis experiments and, in particular, we have
synthesized some mutual exclusion protocols which are guaranteed to enjoy
various properties, such as (i) bounded overtaking, (ii) absence of starvation, and
(iii) maximal reactivity (their formal definition will be given in the paper). We
finally compare our results with those presented in [
The paper is structured as follows. In Section 2 we recall some preliminary notions and terminology. In Section 3 we present our framework for synthesizing concurrent programs and we define the notion of a symmetric concurrent program. In Section 4 we describe our synthesis procedure and the logic program which we use for the synthesis. In Section 5 we present some examples of synthesis of symmetric concurrent programs. Finally, in Section 6 we discuss the related work and some topics that can be investigated in the future. 2
Let us recall some basic notions and terminology we will use. We present: (i) the
syntax of (a variant of) the guarded commands [
The execution of if gc1 8 . . . 8 gcn fi is performed as follows: one of the guarded commands g → c in {gc1, . . . , gcn} whose guard g evaluates to true is chosen, then c is executed; otherwise, if no guard in {gc1, . . . , gcn} evaluates to true then the whole command if . . . fi terminates with failure.
The execution of do gc1 8 . . . 8 gcn od is performed as follows: one of the guarded commands g → c in {gc1, . . . , gcn} whose guard g evaluates to true is chosen, then c is executed and the whole command do . . . od is executed again; otherwise, if no guard in {gc1, . . . , gcn} evaluates to true then the execution proceeds with the next command.
Symmetric Groups. A group G is a pair hS , ◦i, where S is given a set and ◦ is a binary operation on S satisfying the following axioms: (i) ∀x, y ∈ S. x ◦ y ∈ S (closure), (ii) ∀x , y, z ∈ S . (x ◦ y) ◦ z = x ◦ (y ◦ z ) (associativity), (iii) ∃e ∈ S. ∀x ∈ S.e ◦ x = x ◦ e = x (identity element), and (iv) ∀x ∈ S. ∃y ∈ S. x ◦ y = y ◦ x = e (inverse element). The order of a group G is the cardinality of S. For any x ∈ S, for any n ≥ 0, we write xn to denote the term x ◦ . . . ◦ x with n occurrences of x. We stipulate that x0 is e.
A group G is said to be cyclic iff there exists an element x ∈ S, called a generator, such that S = {xn | n ≥ 0}. We write Gx to denote the cyclic group generated by x.
We denote by Perm(S) the set of all permutations (that is, bijections) on
the set S. Perm(S) is a group whose operation ◦ is function composition and the
identity e is the identity permutation, denoted id. The order of a permutation p
on a finite set S is the smallest natural number n such that pn = id .
Computation Tree Logic. Computation Tree Logic (CTL) is a propositional
branching time temporal logic [
Let Elem be a finite set of elementary propositions ranged over by b. The syntax of a CTL formula ϕ is as follows:
ϕ ::= b | ϕ1 ∧ ϕ2 | ¬ϕ | EX ϕ | EG ϕ | E[ϕ1 U ϕ2] Let us introduce the following abbreviations: (i) ϕ1 ∨ ϕ2 for ¬(¬ϕ1 ∧ ¬ϕ2), (ii) EFϕ for E[true U f ] (iii) AG ϕ for ¬EF ¬ϕ, (iv) AFϕ for ¬EG ¬ϕ, (v) A[ϕ1 U ϕ2] for ¬E[¬ϕ2 U (¬ϕ1 ∧ ¬ϕ2)] ∧ ¬EG ¬ϕ2, (vi) AX ϕ for ¬EX ¬ ϕ, (vii) A[ϕ1 R ϕ2] for ¬E[¬ϕ1 U ¬ϕ2], and (viii) E[ϕ1 R ϕ2] for ¬A[¬ϕ1 U ¬ϕ2].
We define the semantics of CTL by giving a Kripke structure K = hS, S0, λ, Ri, where: (i) S is a finite set of states, (ii) S0 ⊆ S is a set of initial states, (iii) R ⊆ S × S is a total transition relation (thus, ∀u ∈ S, ∃v ∈ S, hu, vi ∈ R), and (iv) λ : S → P (Elem ) is a total, labelling function that assigns to every state s ∈ S a subset λ(s) of the set Elem .
For reasons of simplicity, when the set of the initial states is a singleton {u}, we will feel free to identify {u} with u.
A path π in K from a state is an infinite sequence hs0, s1, . . .i of states such that, for all i ≥ 0, hsi, si+1i ∈ R. For i ≥ 0, we denote by πi the i -th element of π. The fact that a CTL formula ϕ holds in a state s of a Kripke structure K will be denoted by K, s ϕ. For any CTL formula ϕ and state s, we define the relation K, s ϕ as follows:
K, s b iff b ∈ λ(s) K, s ¬ ϕ iff K, s ϕ does not hold K, s ϕ1 ∧ ϕ2 iff K, s ϕ1 and K, s ϕ2 K, s EX ϕ iff there exists hs, ti ∈ R such that K, t ϕ K, s E[ϕ1 U ϕ2] iff there exists a path π = hs, s1, . . .i in K and i ≥ 0 such that K, πi ϕ2 and for all 0 ≤ j < i, K, πj ϕ1 K, s EG ϕ iff there exists a path π such that
π0 = s and for all i ≥ 0, K, πi ϕ 2.1
Answer Set Programming
Answer set programming (ASP) is a declarative programming paradigm based
on the answer set semantics of logic programs [
a1 ∨ . . . ∨ ak ← ak+1 ∧ . . . ∧ am ∧ not am+1 ∧ . . . ∧ not an
where a1, . . . , ak, . . . , an (for k ≥ 0, n ≥ k) are atoms and ‘not’ denotes negation as
failure [
An interpretation I of a program Π is a subset of the Herbrand base. The Gelfond-Lifschitz transformation of a program Π with respect to an interpretation I is the program ΠI = {head (r ) ← pos(r ) | r ∈ Π ∧ neg(r ) ∩ I = ∅}. An interpretation M is said to be an answer set of Π iff M is the least Herbrand model of ΠM . The answer set semantics of Π assigns to Π a set of answer sets, denoted ans(Π). Given an answer set M ∈ ans(Π) and an atom a, we write M |= a to denote that a ∈ M . 3
Let P = {P1, . . . , Pk} be a finite set of processes. With every process Pi ∈ P we associate a variable si, called the local state, ranging over a finite domain L, which is the same for all processes. The variable si can be tested and modified by Pi only. All processes may test and modify also a shared variable x, which ranges over a finite domain D.
A concurrent program consists of a finite set P of processes that are executed in parallel and interact with each other through a communication protocol realized by a set of commands acting on the shared variable x. Here is the formal definition of a concurrent program.
Definition 1 (k -Process Concurrent Program). Let L be a set of local states and D be a domain of the shared variable x. For any k > 1, a k -process concurrent program C is a command of the form:
C :
s1 := l1; . . . ; sk := lk; x := d0; do P1 8 . . . 8 Pk od where s1, . . . , sk, x ∈ Var , l1, . . . , lk ∈ L, and d0 ∈ D.
Every process Pi in P1 8 . . . 8 Pk is a guarded command of the form: Pi : gc : true → if gc1 8 . . . 8 gcn fi Every guarded command gc in gc1 8 . . . 8 gcn is of the form: where l, l′ ∈ L and d, d′ ∈ D.
We shall use the guarded command si = l ∧ x = d → skip as a shorthand for si = l ∧ x = d → si := l; x := d. The command s1 := l1; . . . ; sk := lk; x := d0; is called initialization of C.
Example 1. Let L be the set {t, u} and D be the set {0, 1}. A 2-process concurrent program C is:
s1 := t; s2 := t; x := 0 ; do P1 8 P2 od where P1 and P2 are defined as follows: P1 : true → if P2 : true → if
s1 = t ∧ x = 0 → s1 := u; x := 0; s2 = t ∧ x = 1 → s2 := u; x := 1; 8 s1 = t ∧ x = 1 → skip; 8 s2 = t ∧ x = 0 → skip; 8 s1 = u ∧ x = 0 → s1 := t; x := 1; 8 s2 = u ∧ x = 1 → s2 := t; x := 0; fi fi This program is the familiar program for two processes, each of which either ‘thinks’ in its noncritical section (si = t) or ‘uses a resource’ in its critical section (si = u). The shared variable x gives each process its turn to enter the critical section: if x = 0, process P1 is in its critical section, and if x = 1, process P2 is in its critical section.
Now we introduce the semantics of concurrent programs by using Kripke structures. We model a state u of a k-process concurrent program C by a (k + 1)-tuple hl1, . . . , lk, di, where: (i) the first k components are the values of the local state variables s1, . . . , sk, and (ii) d is the value of the shared variable x.
Definition 2 (Kripke Structure Associated with a k -Process Concurrent Program). Let C be a k -process concurrent program of the form C :
s1 := l1; . . . ; sk := lk; x := d0; do P1 8 . . . 8 Pk od where the li’s belong to L and d0 belongs to D. The Kripke structure K associated with C is the 4-tuple hS, S0, R, λi, where: (i) the set S of states is Lk × D, (ii) the set S0 of initial states is the singleton {hl1, . . . , lk, d0i}, (iii) the set R ⊆ S ×S of transitions {hu, vi | i, j ∈ {1, . . . , k} ∧ si = l ∧ x = d → si := l′; x := d′ in Pi ∧ u(si) = l ∧ u(x) = d ∧ v(si) = l′ ∧ v(x) = d′ ∧ u 6= v ∧ ∀j 6= i, u(sj) = v(sj)}, where for all states t ∈ S, for all variables x ∈ Var , t(x) denotes the value of the variable x in t, and (iv) for all states t of the form hl1, . . . , lk, di, the value λ(t) is defined to be {s1 = l1, . . . , sk = lk, x = d}.
The set Elem of the elementary propositions is the set St∈S λ(t).
We make the following assumptions about k -process concurrent programs.
(i) Since, by definition, the transition relation R of any Kripke structure is total,
we have that every concurrent program C we consider, is nonterminating, in the
sense that, in every state there exists a process Pi of C and a guarded command
g → c of Pi such that: (i.1) g evaluates to true, and (i.2) c cannot be abbreviated
to skip. This assumption restricts the class of concurrent programs we consider.
(ii) Every k-process concurrent program consists of deterministic processes, that
is, for i = 1, . . . , k, in every state, at most one guard of the guarded commands
of process Pi evaluates to true (a similar assumption is made in [
Note that the usual assumption that every guarded command is executed atomically (in the sense that only one process at a time among the processes of a concurrent program is selected and executed) is taken into account in an implicit way when constructing the transition relation R of the Kripke structure. Example 2. Given the 2-process symmetric concurrent program C of Example 1, the associated Kripke structure hS, {s0}, R, λi is depicted in Figure 1. We depict it as a graph whose nodes are the states in S and whose edges represent the transitions in R. The set S of states includes the four state depicted in Figure 1 and also the states ht, u, 0i, hu, t, 1i, hu, u, 0i, and hu, u, 1i, which have not been depicted because they are not reachable from the initial state ht, t, 0i. Each transition from state u to state v is associated with the guarded command g → c whose guard g evaluates to true in u. For the labelling function λ, we have that λ(ht, t, 0i) is {s1 = t, s2 = t, x = 0} and, similarly, for the other states.
Having defined the Kripke structure associated with a given program, now we can define the notion of a program satisfying a given behavioural property. Definition 3 (Satisfaction relation for a Concurrent Program). Let C be a k -process concurrent program, K be the Kripke structure associated with C, s0 be the initial state of K, and ϕ be a CTL formula. We say that C satisfies ϕ, denoted C |= ϕ, iff K, s0 |= ϕ.
Example 3. Let us consider the 2-process concurrent program C defined in Example 1. We associate with the local states t (short for ‘think’) and u (short for ‘use’) two regions of code, called the noncritical section and the critical section, respectively. We require that the region of code associated with state u should be executed in a mutually exclusive way. This is formalized by the CTL formula s1 = t ∧ x= 0 → s1 := u; x:= 0
s1 = u ∧ x= 0 → s1 := t; x:= 1 ht, t, 0i ϕ =def AG[¬(s1 = u ∧ s2 = u)], and we have that C |= ϕ holds because for the Kripke structure K of Example 2 (see Figure 1), we have that K, s0 |= ϕ (indeed, there is no path starting from the initial state s0 = ht, t, 0i which leads the system to either the state hu, u, 0i or the state hu, u, 1i).
Often, in our setting a k -concurrent program consists of symmetric processes,
the symmetry being determined by the fact that, for any two processes Pi and Pj,
for i 6= j, we have that Pj can be obtained from Pi by permuting the values of the
shared variable x in the guarded commands. Indeed, as shown in Example 1, the
guarded commands in P2 can be obtained from those in P1 by interchanging 0
and 1. In practice, the property of symmetry is very common in many
concurrent programs, and our task is precisely the one of automatically synthesizing
symmetric processes. This observation motivates a notion of symmetry which we
now introduce by using cyclic groups. A similar approach has been followed for
the automated verification of concurrent systems in [
Definition 4 (k -Generating Function). Given an integer k > 1, and a finite domain D, we say that f ∈ Perm(D ) is a k-generating function iff either f = id or f is a generator of a cyclic group Gf = {id , f, f 2, . . . , f k−1} of order k. Let us introduce the following notation. Given a guarded command gc of the form:
si = l ∧ x = d → si := l′; x := d′; and a k-generating function f , we denote by f (gc) the guarded command: s(i mod k)+1 = l ∧ x = f (d) → s(i mod k)+1 := l′; x := f (d′); Definition 5 (k -Process Symmetric Concurrent Program). Given a k-generating function f, a k-process symmetric concurrent program C is a command of the form:
C : s1 := l0; . . . ; sk := l0; x := d0; do P1 8 . . . 8 Pk od where, for all processes Pi, for all guarded commands gc, gc is in Pi iff f (gc) is in P(i mod k)+1 .
Example 4. Let us consider the 2-process concurrent program C of Example 1. The group Perm(D) of permutations over D = {0, 1} is made out of the following two permutations only: f1 = {h0, 0i, h1, 1i} and f2 = {h0, 1i, h1, 0i}. The 2-generating function f2 shows that the concurrent program C is symmetric. P1 : true → if
s1= t ∧ x = 0 → s1:= u; x := 0; 8 s1= t ∧ x = 1 → skip; 8 s1= u ∧ x = 0 → s1:= t; x := 1; fi
P2 : true → if
s2= t ∧ x=f2(0) → s2:= u; x:=f2(0); 8 s2= t ∧ x=f2(1) → skip; 8 s2= u ∧ x=f2(0) → s2:= t; x:=f2(1); fi By definition, one can generate a k-process symmetric concurrent program C from one of the processes in C by applying the generating function f . Moreover, it is often the case that all processes of a given program C also share additional structural properties, besides those determined by f . For instance, in the case of Example 4, we have that both process P1 and P2 may move from the local state t to the local state u, or from t to t, or from u to t. These additional structural properties define a local transition relation T ⊆ L×L which together with the k -generating function f , defines a so called symmetric program structure Σ = hf, T i. A pair hl, l′i in T will also be denoted by l 7→ l′.
Our synthesis problem can be defined as follows.
Definition 6 (Synthesis Problem of a k -Process Symmetric Concurrent Program). The synthesis problem of a k-process symmetric concurrent program C starting from: (i) a CTL formula ϕ, and (ii) a symmetric program structure Σ = hf, T i, where f is a k-generating function and T is a local transition relation, consists in finding C such that C |= ϕ holds.
Note that there exists a CTL formula that characterizes the set of initial states. In particular, the initial state hl1, . . . , lk, d0i can be characterized by the CTL formula s1 = l1 ∧ . . . ∧ sk = lk ∧ x = d0, where we assume that each conjunct belongs to Elem. However, for reasons of simplicity, we assume that the initial state s0 is given to our synthesis procedure as an additional input (see clause 1 of the logic program Πϕ of Definition 7). 4
In this section we present our synthesis procedure based on ASP. We encode the desired behavioural property ϕ of our k -process concurrent program to be synthesized as a logic programs Πϕ, and the desired structural property Σ as a logic programs ΠΣ. Programs Πϕ and ΠΣ are defined in the following Definition 7 and 8, respectively.
Definition 7 (Logic program encoding a behavioural property). Let ϕ be a CTL formula expressing a behavioural property. The logic program Πϕ encoding ϕ is as follows: 1. ← not sat (s0, ϕ) · · · 11.k tr (s(S1, . . . , Sk, X), s(S1′, . . . , Sk′, X′)) ← reachable(s(S1, . . . , Sk, X)) ∧ gc(k, Sk, X, Sk′, X′) ∧ hSk, Xi 6= hSk′, X′i 12. ← not out(S) ∧ reachable(S) 13. out (S) ← tr (S, Z) 14. reachable(s0) ← 15. reachable(S) ← tr (Z, S) where the predicates are defined as follows: (i) sat (U, F ) holds iff the formula F holds in state U , (ii) elem(b, u) holds iff b ∈ λ(u), that is, the elementary proposition b holds in state u, (iii) satpath(U, V, F ) holds iff there exists a path from state U to state V such that every state in that path satisfies the formula F , (iv) tr (s(S1, . . . , Sk, X), s(S1′, . . . , Sk′, X′)) holds iff the pair of states hhS1, . . . , Sk, Xi, hS1′, . . . , Sk′, X′ii belongs to the transition relation R of the Kripke structure associated with the program C to be synthesized, and (v) the predicates out and reachable force the relation R to be total (in particular, out(S) holds iff from state S there is an outgoing edge, and reachable(S) holds iff there is a path from the initial state s0 to state S.) Rule 1 is required for ensuring that ϕ holds in the initial state s0 representing the initialization s1 := l0; . . . ; sk := l0; x := d0 of the k -process symmetric concurrent program to be synthesized. Rule 11.i defines the interleaved execution of the guarded commands, that is, for all states U and V, tr(U, V ) holds iff U is a reachable state, and there exists a guarded command gc of process Pi whose guard evaluates to true in U and whose execution leads from state U to state V . Definition 8 (Logic program encoding a structural property). Let L be the set of local states and D be the domain of the shared variable. Let Σ = hf, T i be a symmetric program structure of a k -process symmetric concurrent program. The logic program ΠΣ is defined as follows: 1.1 WhS′,X′i∈Next(hS1,Xi) gc(1, S1, X, S′, X′) ← reachable(S1, S2, . . . , Sk, X)
← gc(1, S, X, S′, X′) ∧ gc(1, S, X, S′′, X′′) ∧ hS′, X′i 6= hS′′, X′′i 2.1 gc(2, S, f (X), S′, f (X′)) ← gc(1, S, X, S′, X′)
← gc(2, S, X, S′, X′) ∧ not ps(2, S, X) 2.3 ps (2, S2, X) ← reachable(S1, S2, . . . , Sk, X)
. . . k.1 gc(k, S, f (X), S′, f (X′)) ← gc(k−1, S, X, S′, X′) k.2
← gc(k, S, X, S′, X′) ∧ not ps(k, S, X) k.3 ps (k, Sk, X) ← reachable(S1, S2, . . . , Sk, X) where: (i) gc(i, S, X, S′, X′) holds iff si = l ∧ x = d → si := l′; x := d′ is in Pi, (ii) f is a k -generating function, (iii) ps(i, S, X) holds iff there exists a reachable state of the form hS1, . . . , Si−1, S, Si+1, . . . , Sk, Xi, and (iv) for all l ∈ L, d ∈ D, Next(l, d) = {hl′, d′i | l 7→ l′ ∈ T ∧ d′ ∈ D}.
Rules 1.1 and 1.2 generate a set of guarded commands for process P1. The disjunction in the head of Rule 1.1 is over all possible guarded commands that P1 may execute. The set of those guarded commands is defined using the sets Next(l, d), one for each l ∈ L and d ∈ D. The integrity constraint 1.2 enforces the generation of a set of guarded commands in which any two guards of the guarded commands in P1 are mutually exclusive (recall that we consider only deterministic processes).
For j = 2, . . . , k, Rules j.1, j.2 and j.3 realize Definition 5. We use Rule j.1 to derive a guarded command in Pj from a guarded command of the process Pj−1. Rule j.2 ensures that for every guarded command g → c derived by j.1, there exists a reachable state U such that in U the guard g evaluates to true.
Now we present a theorem establishing the correctness of our synthesis procedure. It relates the k-process symmetric concurrent programs satisfying ϕ with the answer sets of the logic program Πϕ ∪ ΠΣ. Obviously, the correctness of the synthesis procedure implies also the correctness of the programs Πϕ and ΠΣ encoding the behavioural properties and the structural properties, as specified in Definition 7 and 8, respectively.
Theorem 1 (Correctness of Synthesis). Let Π = Πϕ ∪ ΠΣ be the logic program obtained, as specified by Definitions 7 and 8, from: (i) a CTL formula ϕ and (ii) a symmetric program structure Σ = hf, T i. Then,
s1 := l0; . . . ; sk := l0; x := d0; do P1 8 . . . 8 Pk od |= ϕ iff there exists an answer set M in ans(Π) such that ∀i ∈ {1, . . . , k}, ∀l, l′ ∈ L, ∀d, d′ ∈ D,
si = l ∧ x = d → si := l′; x := d′ is in Pi iff M |= gc(i, l, d, l′, d′). 5
In this section we present some experimental results obtained by applying our synthesis procedure to mutual exclusion protocols. All experiments have been performed on an Intel Core 2 Duo E7300 2.66GHz under the Linux operating system.
The first synthesis we did is the one of a simple program, called 2-mutex -1, for two processes enjoying the mutual exclusion property only, and then we progressively increased the number of properties that the synthesized program should AG ¬(si = u ∧ sj = u)
AG (si = w → AF si= u) satisfy (see Table 1). In that table the program k-mutex -p denotes a synthesized program for k processes satisfying p behavioural properties. For instance, program 2-mutex -4 is the synthesized program that works for 2 processes and enjoys the four behavioural properties: (i) ME (mutual exclusion), (ii) SF (starvation freedom), (iii) BO (bounded overtaking), and (iv) MR (maximal reactivity), defined by CTL formulas as follows. (i) Mutual Exclusion, that is, it is not the case that process Pi is in its critical section (si = u), and process Pj is in its critical section (sj = u) at the same time: for all i, j in {1, . . . , k}, with i 6= j, (ME ) (SF ) (ii) Starvation Freedom, that is, if a process is waiting to enter the critical section (si = w), then after a finite amount of time, process Pi will execute its critical section (si = u): for all i in {1, . . . , k}, (iii) Bounded Overtaking, that is, while process Pi is in its waiting section, any other process Pj exits from its critical section at most once: for all i, j in {1, . . . , k},
AG ((si = w ∧ sj = u) → AF (sj = t ∧ A[¬(sj = u) U si = u])) (BO ) (iv) Maximal Reactivity, that is, if process Pi is waiting to execute the critical section and all other processes are executing their noncritical sections, then in the next state Pi will enter its critical section: for all i in {1, . . . , k}, AG ((si = w ∧ Vj∈{1,...,k}\{i} sj = t) → EX si = u) (MR) In our synthesis experiments we have made the following choices for s0, L, D, f , and T .
The initial state s0 is ht, t, 0i and ht, t, t, 0i for the 2- and 3-process symmetric concurrent programs, respectively.
The set L of the local states for the variables si’s is {t, w, u}, where t represents the noncritical section, w represents the waiting section, and u represents the critical section.
The domain D of the shared variable x is a finite set of natural numbers whose cardinality |D| depends on: (i) the number k of the processes to be synthesized, and (ii) the properties that the concurrent program should satisfy. The value of |D| is not known a priori, and we guess it at the beginning of our synthesis task. If the synthesis fails, we increase the value of |D|, hoping for a successful synthesis with a larger value of |D|.
The k -generating function f is chosen among the following ones: (i) id is the identity function, (ii) f1 = {h0, 1i, h1, 0i}, (iii) f2 = {h0, 1i, h1, 0i, h2, 2i}, and (iv) f3 = {h0, 1i, h1, 2i, h2, 0i}.
The local transition relation T is {t 7→ w, w 7→ w, w 7→ u, u 7→ t}. The pair t 7→ w denotes that, once the noncritical section has been executed, a process enters the waiting section. The pairs w 7→ w and w 7→ u denote that a process may repeat (possibly an unbounded number of times) the execution of its waiting section and then may enter its critical section. The pair u 7→ t denotes that, once the critical section has been executed, a process enters its noncritical section. 6 7 3 3 2 5 8 10
Satisfied Properties |D| |ans(Π)| Time
In Figures 2 and 3 we present the syntax and the semantics of the synthesized
program, called 2-mutex -4, for the 2-process mutual exclusion problem described
in Example 3. (Program 2-mutex -4 is essentially the same as the Peterson
algorithm [
Two well known, early works on synthesis of concurrent programs were those by
Emerson and Clark [
In [
Similarly to [
In [
s1 = t ∧ x = 0 → s1 := w; x := 2; 8 s1 = t ∧ x = 1 → s1 := w; x := 2; 8 s1 = t ∧ x = 2 → s1 := w; x := 1; 8 s1 = w ∧ x = 0 → s1 := u; x := 0; 8 s1 = w ∧ x = 1 → skip; 8 s1 = w ∧ x = 2 → s1 := u; x := 2; 8 s1 = u ∧ x = 2 → s1 := t; x := 1; 8 s1 = u ∧ x = 0 → s1 := t; x := 2; fi
P2 : true → if
s2 = t ∧ x = 0 → s2 := w; x := 2; 8 s2 = t ∧ x = 1 → s2 := w; x := 2; 8 s2 = t ∧ x = 2 → s2 := w; x := 0; 8 s2 = w ∧ x = 0 → skip; 8 s2 = w ∧ x = 1 → s2 := u; x := 1; 8 s2 = w ∧ x = 2 → s2 := u; x := 2; 8 s2 = u ∧ x = 2 → s2 := t; x := 0; 8 s2 = u ∧ x = 1 → s2 := t; x := 2; fi
O(N 3) algorithm to construct an automaton satisfying a formula of a particular class of LTL specifications.
We closely follow the approaches of [
In order to reduce the search space of our synthesis problem, we have used
a notion of symmetric concurrent programs which is similar to the one which
was introduced in [
Similarly to Attie and Emerson [
We have implemented our synthesis method in Answer Set Programming
(ASP). One advantage of our method over [
To the best of our knowledge, there is only one paper by Heymans,
Nieuwenborgh and Vermeir [
As future work we plan to explore various techniques for reducing the search
space of the synthesis procedure and, thus, we hope to synthesize protocols
for a larger number of processes and more complex properties to be guaranteed.
Among these techniques we envisage to apply those used in compositional model
checking [