=Paper=
{{Paper
|id=Vol-2710/paper23
|storemode=property
|title=A Formally Verified SMT Approach to True Concurrency
|pdfUrl=https://ceur-ws.org/Vol-2710/paper23.pdf
|volume=Vol-2710
|authors=Juliana K. F. Bowles,Marco B. Caminati
|dblpUrl=https://dblp.org/rec/conf/cilc/BowlesC20
}}
==A Formally Verified SMT Approach to True Concurrency==
https://ceur-ws.org/Vol-2710/paper23.pdf
A Formally Verified SMT Approach to True
Concurrency?
Juliana K. F. Bowles[0000−0002−5918−9114] and Marco
B. Caminati[0000−0002−4529−5442]
School of Computer Science, University of St Andrews
St Andrews KY16 9SX, United Kingdom
{jkfb|mbc8}@st-andrews.ac.uk
Abstract. Many problems related to distributed and parallel systems,
such as scheduling and optimisation, are computationally hard, thereby
justifying the adoption of SMT solvers. The latter provide standard
arithmetic as interpreted functions, naturally leading to express concur-
rent executions as a linearly-ordered sequentialisation (or interleaving)
of events, which have an obvious correspondence with integer segments
and therefore permit to take advantage of such arithmetical capabilities.
However, there are alternative semantic approaches (also known as true
concurrent) not imposing the extra step of interleaving events, which
brings the question of how to computationally exploit SMT solvers in
these approaches. This paper presents a solution to this problem, and in-
troduces a metric, made possible by adopting a true concurrent paradigm,
which relates mutually distinct solutions of a family of distributed optimi-
sation problems. We also contribute an original, computational definition
of degree of parallelism, which we compare with the existing ones. Finally,
we use theorem proving to formally certify a basic correctness property
of our true concurrent approach.
1 Introduction and Related Work
There are many possible models to capture the behaviour of distributed and
parallel systems. Here we use labelled (prime) event structures [24], or event
structures for short. Event structures have been widely studied in the literature,
and have been used to give a true concurrent semantics to process calculi such as
CCS, CSP, SCCS and ACP (e.g., [23]). The advantages of prime event structures
include their underlying simplicity and how they naturally describe fundamental
notions present in behavioural models including sequential, parallel and iterative
behaviour (or the unfoldings thereof) as well as nondeterminism (cf. [14]), and
are hence our model of choice. Event structures consist of sets of events and
?
This research is supported by MRC grant MR/S003819/1 and Health Data Research
UK, an initiative funded by UK Research and Innovation, Department of Health
and Social Care (England) and the devolved administrations, and leading medical
research charities. Copyright c 2020 for this paper by its authors. Use permitted
under Creative Commons License Attribution 4.0 International (CC BY 4.0).
binary relations over events to represent these notions. When used to capture the
behaviour of a system, for example, event structures can be further equipped with
labelling (total or partial) functions that associate information to these events,
such as the action performed, action synchronisations, or any additional metric
that may be relevant within the context. For instance, in a medical context an
event may be associated with taking a particular medication, and a measure of
interest may be the efficacy of the chosen medication for the underlying treatment.
Event structures have well-defined composition operators (cf. e.g., [18]). How-
ever, these composition mechanisms ignore labels and are hence inadequate for
our use here. In practice we are not interested in computing the composition of
models, but rather in finding optimal paths of execution in such a composition
with respect to a certain measure of interest (usually a certain integer value
which we want to maximise or minimise). Again, within a medical context this
may be to maximise the efficacy of the medications given to patients following
multiple treatment plans (which may be the case if patients have multimorbidi-
ties, i.e., multiple ongoing chronic conditions). In this case, we are searching for
optimal treatment plans which also avoid adverse drug reactions between chosen
medications (i.e., maximise efficacy whilst minimising adverse reactions).
When measures of interest can be quantified, we can make use of SMT
(Satisfiability Modulo Theories) solvers to search for the optimal solution. We
have used the SMT solver Z3 [17] in our earlier work (see for instance [5,6,7]).
However, in that work we have ignored the true concurrent nature of event
structures and treated the inherent parallelism within executions as interleaving.
In this paper, we turn our attention to the problem of computing and se-
lecting trace executions in a true-concurrent manner, as opposed to an implicit
non-deterministic choice among allowed sequentialisations (or interleaving) of
events. While work exists providing theoretical frameworks to characterise and
reason about true-concurrency [1], [10], [15], true-concurrent approaches to the
computational problem introduced above are rare. Other existing works we are
aware of (see, for example, [12]) deal with notions of distance between different
event structures, rather than between trace executions of one event structure.
In [16] a problem similar to the one considered here is studied, but within the
theoretical framework of Petri nets, and without including a numerical interaction
between sets of concurrent events to influence the execution choice, as we do here:
there, the focus is more on the theoretical study of the complexity associated
with checking the optimality of a number of resources (concurrency threshold)
for the execution of a given parallel process. Our work presents similar differ-
ences with [9], where an encoding of timed BPMN models into rewriting logic is
presented; this permits to use the rewriting logic implementation Maude [8] in
order to reflect about a notion of parallelism degree.
The contributions we provide are: an SMT-viable model for a true-concurrent
handling of trace executions, a notion of metric to be able to choose among such
executions, and, at the same time, to quantify the degree of concurrency of a trace
execution; finally, a formal verification of a basic sanity property of our approach
through the theorem prover Isabelle/HOL, where Isabelle is foundation-agnostic
proof assistant and Isabelle/HOL is the strain based on higher-order logic (HOL)
[19]1
This paper is structured as follows. Section 2 describes the formal model
used, how configurations and paths/traces of executions are defined, as well as
what resources we care to maximise/minimise when searching for the optimal
path. Our SMT-based formulation of the problem is shown in Section 3 and
how verification is done is described in Section 4. This is followed by concluding
remarks in Section 5.
2 Formal Model
In an event structure, we have a set of event occurrences together with binary
relations for expressing causal dependency (called causality) and nondeterminism
(called conflict). The causality relation implies a (partial) order among event
occurrences, while the conflict relation expresses how the occurrence of certain
events excludes the occurrence of others. From the two relations defined over
the set of events, a further relation is derived, namely the concurrency relation
co. Two events are concurrent if and only if they are completely unrelated, i.e.,
neither related by causality nor by conflict.
The formal definition of an event structure, as in [14], is as follows.
Definition 1. An event structure is a triple E = (Ev, →∗ , #) where Ev is a
set of events and →∗ , # ⊆ Ev × Ev are binary relations called causality and
conflict, respectively. Causality →∗ is a partial order. Conflict # is symmetric and
0 00 00
irreflexive, and propagates over causality, i.e., e#e ∧ e0 →∗ e ⇒ e#e for all
0 00 0 0
∗ 0 0
e, e , e ∈ Ev. Two events e, e ∈ Ev are concurrent, e co e iff ¬(e → e ∨e →∗
0
e ∨ e#e ). C ⊆ Ev is a configuration iff (1) C is conflict-free: ∀e, e ∈ C¬( e#e0 )
0
and (2) downward-closed: e ∈ C and e0 →∗ e implies e0 ∈ C.
We assume discrete event structures. Discreteness imposes a finiteness con-
straint on the model, i.e., there are always only a finite number of causally related
predecessors to an event, known as the local configuration of the event (written
↓ e). A further motivation for this constraint is given by the fact that every
execution has a starting point or configuration. A maximal configuration is called
a trace. An event e may have an immediate successor e0 according to the order
→∗ , written e → e0 , where → denotes immediate causality iff there is no possible
intermediate event. Fig. 1 shows a visual depiction of a simple event structure.
Here, event e0 marks the initial event, and events e1 #e8 are in conflict. Ac-
cording to conflict propagation, events e1 #e9 are also in conflict. Immediate
causality is shown, and any events not related by causality or conflict are con-
current. For instance, e2 co e6 are concurrent. Two configurations are shown
surrounding some of the events: in red to the left (X1 ), and in green to the right
(X2 ). X1 contains concurrency, whereas X2 does not. Moreover, X1 =↓e7 and
X2 =↓e10 .
1
We will often write just Isabelle in lieu of Isabelle/HOL.
Fig. 1. Example event structure.
To make a connection between the semantic model (an event structure) and
the syntactic model (ignored here) it is describing, we need to associate additional
information to individual events. Let L be a given set of labels.
Definition 2. A labelled event structure over L is a triple M = (Ev, µ, ν) where
µ and ν are partial labelling functions µ : Ev → 2L and ν : Ev → N × N.
Labelled event structures are event structures enriched with two labelling
functions µ and ν. The function µ maps events onto a subset of elements of L.
The labels in the set L either denote formulas (constraints over integer variables,
e.g., x > 9 or y = 5), logical propositions (e.g., pro1) or actions (e.g., ma1). If
for an event e ∈ Ev, µ(e) contains an action α ∈ L, then e denotes an occurrence
of that action α. If µ(e) contains a formula or logical proposition ϕ ∈ L, then ϕ
must hold when e occurs.
The labelling function ν associates to each event its priority and duration,
for instance, ν(e) = (p, d) indicates that p is the priority and d is the duration
associated with e. The higher the value of p, the higher the priority associated to
the event. The duration d indicates the time units spent at event e. Sometimes, we
will write ν1 or ν2 for the function returning only the first or second component
of the pair returned by ν.
Giving different priority values to events is meaningful in the presence of
alternatives (conflicting events), where the highest value can be used to determine
the ideal configuration in a model. For instance, event e2 may have a higher
priority than e8 . Further labels may be added to the framework as partial
functions if required. We call a labelled event structure a model in what follows.
In addition, we define a map Γ specifying the level of conflict between event
labels as follows.
Definition 3. Label conflicts are given by a (possibly partial) function Γ : 2L →
Z.
When we are interested to the value of Γ in a restricted subset of L, we use
the notation (l1 , l2 , v), indicating that l1 and l2 are in conflict with an interaction
score of value v. We consider that the lower the value of v the higher the severity
of the label conflict. This permits to add further expressiveness to our model: for
example, two events may not be in conflict, but the possible choice for their labels
could have a bad interaction score, which could lead to alternative solutions. For
the event structure in Fig. 1, we assume that µ(e4 ) = ma2 and µ(e3 ) = mb2 , and
a label conflict such that Γ ({ma2 , mb2 }) = −100.
Fig. 2. Possible executions of X1 with and without label conflicts.
The labels of some of the events (e3 and e4 in the example) are conflicting
according to Γ . When obtaining the optimal trace execution within the event
structure above we need to make sure label inconsistencies are detected and
avoided. A trace execution that avoids a label conflict is given by an execution of
the configuration X2 . However, this is too restrictive since the priority of e2 is
higher than e8 , and X1 may hence lead to an overall better trace execution. The
label conflicts are only a problem if the events occur simultaneously.
In our earlier approach [7], events in a configuration would be linearised and
hence the label conflict automatically avoided. The loss of parallelism would,
however, be too significant, and instead we want to choose trace executions for
configurations that avoid label conflicts but achieve the best possible measure of
concurrency. Consider a few options for traces execution for X1 shown in Fig. 2.
We show a timeline from left to right and event durations, where overlapping
events denote simultaneous execution. As highlighted, trace1 (shorthand name for
execution number 1 of the trace) is problematic since the simultaneous execution
of e3 and e4 would contribute to a label conflict. Both trace2 and trace3 avoid
label conflicts, but trace2 has a higher degree of concurrency as it takes less time
to execute (more events are executed in parallel). Because the notion of how
many events are executed in parallel seems more complicated to define formally,
we take the execution time as a definition of degree of parallelism. While the two
notions are intuitively strongly correlated, this does not mean that this measure
will pick an execution having the highest number of parallel events at all instants.
Let us focus on a given subset of events C (which could be, for example,
the events in a trace), and introduce the idea of how to associate to different
executions of C a number measuring how parallel they are. The lowest degree of
parallelism will correspond to the number Σe∈C ν2 (e) + τ, given by the sum of
all event durations (yielded by the function ν2 ) and an additional parameter τ
representing idle time in between events. τ is a parameter to describe optional
slack in the execution, and can be set to zero when not needed. The highest
possible (loose) upper bound to the degree of parallelism will correspond to the
maximal duration of an event in C.
In our example, let C1 = {e2 , e3 } and C2 = {e4 , e5 , e6 }. The degree of
concurrency for different executions of C1 would be in the range [2, 3 + τ ], where
ν2 (e2 ) = 1 and ν2 (e3 ) = 2; and for C2 in [2, 4 + τ ] where ν2 (e4 ) = ν2 (e6 ) = 1 and
ν2 (e5 ) = 2. In Fig. 2, executions trace1 and trace2 have the highest degree of
concurrency. In the sequel, we will give a precise definition to this idea of degree
of concurrency, allowing us to compute its exact value for any execution, picked
from the range introduced above.
3 An SMT-oriented Formulation
The efficiency of SMT solvers comes at a price: first, one has to find a formulation
of their problem which must be in first-order logic, because SMT-LIB (the
standardised input format for SMT solvers [3]) is a first-order language, although
with some added interpreted relations (whence the letters M and T in SMT).
Secondly, the SMT-LIB code one obtains after managing to do that is typically
very little readable for a human, as we will see in this section. We will deal with
the first problem in this section, and with the second in Section 4.
We will use the natural index i to range over (1, . . . , n) where n is the number
of models (event structures) we are considering for composition. Since we will need
to impose conditions on all of them, in the sequel we will often implicitly quantify
over i. We denote by Gi the set of ordered pairs representing the immediate
causality relation →i ; that is, given events e0 , e1 in the i-th event structure:
(e0 , e1 ) ∈ Gi ↔ e0 →i e1 .
This is the standard way of representing relations (such as →i ) in set theory. Gi
can also be viewed as the set of edges of a directed graph (given by the transitive
reduction of the partial order →∗i ): this graph-theoretical view will sometimes be
useful and gives us the relevant jargon, allowing us to refer to nodes instead of
events, etc. We also denote with
G := ∪i Gi
the union of all the immediate causality relations and with
Evi := dom Gi ∪ ran Gi
the set of all the events of the i-th event structure (dom and ran take the domain
and the range set, respectively, of any given relation). Finally,
[
Ev := Evi
i
is the set of all the events.
3.1 Trace Selection
Recall that a configuration Xi for Evi is a set of events of Evi which is downward
closed and conflict-free:
∀e0 , e1 ∈ Evi . e0 ∈ Xi ∧ e1 ∈ Xi → ¬(e0 #e1 ) (1)
^
∀e1 ∈ ran (Gi ) .e1 ∈ Xi → e0 ∈ Xi (2)
−1 →
e0 ∈(Gi ) {e1 }
Here R→ represents the function mapping a set to its image set through a given
relation R. We note that, since Gi represents a relation as a set of ordered pairs,
G−1
i is the inverse relation. Further, recall that a configuration Xi is a trace
exactly when it is maximal, that is,
∀Y ⊆ Evi satisfying (1)–(2) , Y ⊆ Xi . (3)
Now, the quantification appearing in (3) is not directly expressible, because
a quantification over relations is second-order logic, and any SMT-LIB theory
is within first-order logic. The mathematical language used in (1), (2) and
3 allows us to convey ideas to the reader in a more compact and, hopefully,
more understandable way than crude SMT-LIB code would. However, it also
hides difficulties such the one just explained, arising from the gap between the
expressiveness of first-order logic and that of standard mathematical notation.
This problem can have several solutions: in [6] we used bit-vectors to represent sets
and, in [7] we showed condition (3) to be equivalent to the following, first-order
ones:
∀e1 ∈ Evi \Xi . ∃e0 ∈ Evi . ((e0 #e1 ∧ e0 ∈ Xi ) ∨ (4)
((e0 , e1 ) ∈ Gi ∧ e0 ∈
/ Xi ))
This allows us to formulate the problem of trace finding in SMT-LIB.
3.2 Concurrent Execution of Traces
The next step is to define a measure of concurrency which will allow us to execute
a given trace (or configuration) without violating the constraints given by the
causality and conflict relations. Since any configuration is conflict-free, we only
need to focus on not violating the causality relation when executing it.
1. Consider that every event in the configuration has a start time and an end
time, with the latter not smaller than the former;
2. Any two ordered events should not overlap;
3. Any successor (according to →∗ ) of an event should happen after it.
These conditions normally leave quite some freedom in the arrangement of the
events for an execution as shown in Fig. 2 for a configuration X1 . A conceptually
simple approach (commonly referred to as interleaving or sequentialising) is to
find a linear order respecting →∗ : this means finding an order morphism from the
configuration (seen as equipped with the partial order →∗ ) to Z (equipped with
its standard linear, total order). This way of handling execution is particularly
well-suited to an SMT solver due to its awareness of integer arithmetics, and is
the one we adopted in [7].
This approach is usually contrasted, in the literature, with the true concurrent
one, whereby the restriction given by this linearisation is dropped, with an
additional number of possible execution arrangements becoming possible which
still comply with the three conditions above. This amounts to permitting to take
advantage of possible parallelism, which gets lost in the interleaving process: in
the latter approach, compliance with conditions (1)-(3) is attained by ruling out
overlaps between any pair of distinct events, thereby including concurrent events
(recall that two events are concurrent if they are not related by →∗ nor by #).
We now introduce an SMT way of
– modelling this increased choice of possible executions for the traces selected
in the previous subsection and
– ranking them according to their efficiency, that is, their degree of concurrency.
It will rely on two functions, s and t, defined on all the events, and returning the
time each of them starts and ends, respectively.
The first constraint we impose on them is that any single event must respect
time:
∀e ∈ Evi .t (e) − s (e) = ν2 (e) . (5)
Let us recall that we assume that our event structures are finite so that,
in particular, we can define a function pi over the set of non-source nodes for
the directed graph ran Gi returning, for each such node, its parent node in the
considered trace Xi which terminates last:
→
pi (e1 ) ∈ Xi ∩ G−1
(
i ({e1 })
∀e1 ∈ ran Gi . −1 →
(6)
∀e0 ∈ Xi ∩ Gi ({e1 }) . t (pi (e1 )) ≥ t (e0 ) .
We have only one requirement to impose on p:
∀e ∈ ran Gi . s (e) ≥ t (p (e)) . (7)
This last requirement can be tightened to ∀e ∈ ran Gi . s (e) = t (p (e)) in case we
are seeking for executions without idle times between subsequent events.
The formulas introduced in this section capture the linearly interleaved (or
sequentialised) executions we described above, but add more possible executions.
Intuitively, the former are the least possible concurrent execution, and in this
sense they are also the least efficient ones. To make this kind of comparison more
precise, we introduce a measure to rank all the different possible executions. This
will give a metric, or distance, between executions according to their degree of
concurrency. Consider, for a given Gi , the event which terminates last in a given
execution of the trace Xi , denoted zi ; it can be described by the formulas
zi ∈ Xi ∩ (ran Gi \ dom Gi ) (8)
∀e ∈ Xi ∩ (ran Gi \ dom Gi ) . t (zi ) ≥ t (e) . (9)
We will consider an execution of Xi less concurrent than another whenever t (zi )
is larger for the former than for the latter. In this sense, we can use, e.g., an
optimising SMT solver [17] to find the most concurrent execution by simply
asking it to minimise the quantity t (zi ). In particular, this definition of amount
of concurrency can be reconciled with the intuition that sequentialised executions
are the least concurrent ones: the number above will not be maximum for such
executions, given a fixed Xi . This fact is also practically useful: since we know
that a linearised execution has maximal duration, and since such duration is
obviously bounded by the sum of all the event durations, we can pass this bound
as an assertion to the SMT solver to reduce its search space when computing a
generic execution.
Finally, among the several possible traces captured by the assertions of
Section 3.1, we want to select the best one (see the example in Section 2). To do
this, we consider one generic trace Xi for each Gi , and describe which labels are
active at a given time y, via the function l:
[
l (y) = b (ρ (e)) (y ∈ [s (e) , t (e)[).
S
e∈ i Xi
Here, ρ (e) describes the selected label for the event e (which is imposed to
be in the set of allowed labels through an assertion we omit here), and b(j) sets
the j-th bit in a bit-vector of length equal to the overall number of all labels.
Therefore, l(y) is a bit-vector whose 1-bits correspond exactly to the labels active
at time y, because the term in the rightmost pair of brackets filters exactly the
active events (note that our convention is that the when the ending time t (e) of
an event ticks, we consider the event instantly off, so that the range in that term
is right-open). We finally ask the SMT solver to maximise
maxi {t(zi )}
X
Γ (l (t)) ,
t=0
where Γ is a function returning the interaction between the labels denoted by
l (t).
4 Verification
We have seen in Section 3.1 how the gap in expressiveness between standard
mathematical notation and the first-order language of SMT solvers can cause
difficulties when translating a mathematical problem for its computation in an
SMT setting. In some cases, reformulations are needed (recall how we passed from
(1) and (2) to (4) earlier). Even when the translation is more straightforward,
several choices affect the final SMT code passed to the solver. One common
choice is to instantiate universal quantifiers appearing in formulas exploiting
the fact that they quantify over finite domains which are easy to compute
separately, because this can considerably help the solver. For example, (9) features
a universal quantifier ranging over a subset of the sinks of Gi , which is easily
computed, for non-trivial graphs, as the set-theoretical difference between the
set all children of some node of Gi and the set of all parents of some node
of Gi . Performing this computation before invoking the SMT solver helps by
removing a universal quantifier and by carefully restricting the possible cases
over which it is instantiated; this kind of pre-processing is done often to obtain
better performing SMT problems, but comes with a significant drawback: the
SMT code thus obtained becomes exceedingly verbose, and, typically, difficult to
peruse. In other words, the final SMT code usually looks extremely different (and
extremely longer) than the original pen-and-paper mathematical formulation of
the problem; in our case, we can compare the concise mathematical formulation
in Section 3 with the final SMT code we effectively run for a simple example, a
small (necessarily truncated) excerpt of which is in Listing 1.1, representing (6)
and (7).
Listing 1.1. SMT macro for (6) and (7), in the case of a small example (excerpt)
( define−fun trueConcurrencySMT ( ) Bool
( let ( ( $x206 ( and true (=> ( isSelected g0 )
(>= ( endTime ( lastParent g1 ) ) ( endTime g0 ) ) ) ) ) )
( let ( ( $x212 ( and ( or false ( and ( isSelected g0 )
(= ( lastParent g1 ) g0 ) ) ) $x206 (= ( idleTime g1 )
(− ( startTime g1 ) ( endTime ( lastParent g1 ) ) ) )
(>= ( idleTime g1 ) 0 ) ) ) ) ( let ( ( $x165 ( isSelected g1 ) ) )
( let ( ( $x195 ( and ( or false ( and $x165
(= ( lastParent g2 ) g1 ) ) ) ( and true (=> $x165
(>= ( endTime ( lastParent g2 ) ) ( endTime g1 ) ) ) )
(= ( idleTime g2 ) (− ( startTime g2 ) ( endTime ( lastParent g2 ) ) ) )
(>= ( idleTime g2 ) 0 ) ) ) ) ( let ( ( $x142 ( isSelected g2 ) ) )
( let ( ( $x180 ( and ( or false ( and $x165 (= ( lastParent g3 ) g1 ) ) )
( and true (=> $x165 (>= ( endTime ( lastParent g3 ) ) ( endTime g1 ) ) ) )
(= ( idleTime g3 ) (− ( startTime g3 ) ( endTime ( lastParent g3 ) ) ) )
(>= ( idleTime g3 ) 0 ) ) ) )
( let ( ( $x146 ( isSelected g3 ) ) ) [ . . . ]
The striking difference between them is clearly a problem when examining
the SMT code and in particular when this code needs to have some degree of
confidence in the result it produces.
However, nobody prevents us from keeping two SMT codes: one (let us call it
code A) closer to the mathematical formulation (and likely less efficient), and
the other (code B) which underwent a series of transformations as hinted just
above. If the SMT solver returns no models satisfying one code and not the
other, then we can be confident about their equivalence, assuming correctness of
the solver. But, more than that, code A is usually compact enough to be easily
formulated within a theorem prover whose foundations entail the first-order logic
(plus arithmetics) featured in an SMT solver, such as Isabelle/HOL [20]. And,
if we manage to do that, we can use existing SMT code generators from within
the theorem prover, which means that the definitions formulated in the theorem
provers can be used both to prove their correctness and to generate code A. On
top of that, we can arbitrarily introduce intermediate equivalent codes between A
and B, if this eases the verification process. We now see a particular application
of this general verification mechanism.
In Isabelle/HOL, we can introduce the following function:
abbreviation ” trueConcur01 ’ G X lastParent startTime endTime
== ∀ child . ( X child & ( ∃ parent . G parent child ) ) →
( X ( lastParent child ) & ( G ( lastParent child ) child ) &
( ∀ parent . ( X parent & G parent child ) →
endTime ( lastParent child ) ≥ endTime parent ) &
startTime ( child ) ≥ endTime ( lastParent ( child ) ) ) ”
It is carefully crafted to be equivalent, as the one in listing 1.1, to (6) and (7)
and to only feature mathematical objects available in the first-order logic of
an SMT solver; this means no sets, no higher-order functions, no lists, etc:
everything is represented as functions and predicates (for example, instead of
writing child ∈ X, we write X child, where X is a predicate, or boolean function).
This allows us, on one hand, to export it to an SMT constant (let us call it
trueConcurrencyIsabelle) taking advantage of the translator provided by Isabelle’s
Sledgehammer tool [4], and to check its equivalence to trueConcurrencySMT
inside an SMT solver (expecting the answer unsat):
( assert ( or
( and trueConcurrencySMT ( not trueConcurrencyIsabelle ) )
( and ( not trueConcurrencySMT ) ( trueConcurrencyIsabelle ) )
)
)
On the other hand, the Isabelle definition can be proved correctness theorems
about, thereby granting automatically that such correctness proofs carry over
to trueConcurrencySMT. Let us focus on a basic property we expect from any
execution, namely that expressed by requirements (2) and (3) of Section 3.2. The
first step is usually to formulate the SMT-friendly Isabelle definition above into
an equivalent one, but possibly more convenient when coming to formal proofs.
This does not compromise the verification efforts because these new definitions
can be provided with formal theorems proving their equivalence to the original
ones. In this case, we will use
abbreviation
” TrueConcur00 ’ P X lastParent startTime endTime ==
∀ child ∈ X ∩ ( Range P ) . ( lastParent ( child ) ∈ X ∩
immediatePredecessors ’ P { child } &
endTime ( lastParent ( child ) ) ≥
Max ( endTime ‘ ( X ∩ ( immediatePredecessors ’ P { child } ) ) ) &
startTime ( child ) ge endTime ( lastParent ( child ) ) ) ” ,
all the relations have been expressed as sets of ordered pairs, the immediate
causality relation G (corresponding to →) has been substituted by its transitive-
reflexive closure P (corresponding to →∗ ), and the infix operator ‘ takes the
image of a set through a function. We note that the custom-defined operator
immediatePredecessors only makes sense for discrete relations; this is not a
problem here, because we are in a finite setting. We omit the relevant equivalence
proof, and only state the main correctness formal theorem:
theorem fixes startTime : : ”_ => nat ” assumes ” wf ( strict P ) ”
” wf ( strict ( P ˆ −1))” ” atomicTimeArrow P startTime endTime ”
” isPo P”
” TrueConcur00 ’ P X lastParent startTime endTime ” shows
”{ e2 ∈ X ∩ events P . e2 |
( ∃ e0 ∈ X ∩ ( strict P )ˆ −1 ‘ ‘{ e2 } .
startTime ( e2)