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 concurrent 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 introduces a metric, made possible by adopting a true concurrent paradigm, which relates mutually distinct solutions of a family of distributed optimisation problems. We also contribute an original, computational de nition 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.
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 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 e cacy of the chosen medication for the underlying treatment.
Event structures have well-de ned composition operators (cf. e.g., [18]). However, 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 nding 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 e cacy of the medications given to patients following multiple treatment plans (which may be the case if patients have multimorbidities, 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 e cacy whilst minimising adverse reactions).
When measures of interest can be quanti ed, we can make use of SMT (Satis ability 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 selecting 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 di erent 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 in uence 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 di erences 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 re ect 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; nally, a formal veri cation 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 con gurations and paths/traces of executions are de ned, 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 veri cation is done is described in Section 4. This is followed by concluding remarks in Section 5. 2
In an event structure, we have a set of event occurrences together with binary relations for expressing causal dependency (called causality) and nondeterminism (called con ict ). The causality relation implies a (partial) order among event occurrences, while the con ict relation expresses how the occurrence of certain events excludes the occurrence of others. From the two relations de ned 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 con ict.
The formal de nition of an event structure, as in [14], is as follows.
De nition 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
con ict, respectively. Causality ! is a partial order. Con ict # is symmetric and
irre exive, and propagates over causality, i.e., e#e0 ^ e0 ! e00 ) e#e00 for all
e; e0 ; e00 2 Ev. Two events e; e0 2 Ev are concurrent, e co e0 i :(e ! e0 _ e0 !
e _ e#e0 ). C Ev is a con guration i (
We assume discrete event structures. Discreteness imposes a niteness constraint on the model, i.e., there are always only a nite number of causally related predecessors to an event, known as the local con guration of the event (written # e). A further motivation for this constraint is given by the fact that every execution has a starting point or con guration. A maximal con guration is called a trace. An event e may have an immediate successor e0 according to the order ! , written e ! e0, where ! denotes immediate causality i 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 con ict. According to con ict propagation, events e1#e9 are also in con ict. Immediate causality is shown, and any events not related by causality or con ict are concurrent. For instance, e2 co e6 are concurrent. Two con gurations 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.
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.
De nition 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 2 Ev, (e) contains an action 2 L, then e denotes an occurrence of that action . If (e) contains a formula or logical proposition ' 2 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 rst or second component of the pair returned by .
Giving di erent priority values to events is meaningful in the presence of alternatives (con icting events), where the highest value can be used to determine the ideal con guration 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 de ne a map labels as follows.
specifying the level of con ict between event De nition 3. Label con icts are given by a (possibly partial) function Z: : 2L !
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 con ict with an interaction score of value v. We consider that the lower the value of v the higher the severity of the label con ict. This permits to add further expressiveness to our model: for example, two events may not be in con ict, 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 con ict such that (fma2; mb2g) = 100.
The labels of some of the events (e3 and e4 in the example) are con icting 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 con ict is given by an execution of the con guration 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 con icts are only a problem if the events occur simultaneously.
In our earlier approach [7], events in a con guration would be linearised and hence the label con ict automatically avoided. The loss of parallelism would, however, be too signi cant, and instead we want to choose trace executions for con gurations that avoid label con icts 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 con ict. Both trace2 and trace3 avoid label con icts, 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 de ne formally, we take the execution time as a de nition 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 di erent executions of C a number measuring how parallel they are. The lowest degree of parallelism will correspond to the number e2C 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 = fe2; e3g and C2 = fe4; e5; e6g. The degree of concurrency for di erent 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 de nition to this idea of degree of concurrency, allowing us to compute its exact value for any execution, picked from the range introduced above. 3
The e ciency of SMT solvers comes at a price: rst, one has to nd a formulation of their problem which must be in rst-order logic, because SMT-LIB (the standardised input format for SMT solvers [3]) is a rst-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 rst 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) 2 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 := [iGi Ev := [ Evi
i 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, is the set of all the events. 3.1
Trace Selection
(
e0 2 Xi e02(Gi 1)!fe1g 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, Gi 1 is the inverse relation. Further, recall that a con guration Xi is a trace exactly when it is maximal, that is, 8Y
Evi satisfying (
Xi:
Now, the quanti cation appearing in (
((e0#e1 ^ e0 2 Xi) _ ((e0; e1) 2 Gi ^ e0 2= Xi)) This allows us to formulate the problem of trace nding in SMT-LIB. The next step is to de ne a measure of concurrency which will allow us to execute a given trace (or con guration) without violating the constraints given by the causality and con ict relations. Since any con guration is con ict-free, we only need to focus on not violating the causality relation when executing it. 1. Consider that every event in the con guration 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 con guration X1. A conceptually simple approach (commonly referred to as interleaving or sequentialising) is to nd a linear order respecting ! : this means nding an order morphism from the con guration (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 (
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 e ciency, that is, their degree of concurrency. It will rely on two functions, s and t, de ned on all the events, and returning the time each of them starts and ends, respectively.
The rst constraint we impose on them is that any single event must respect
time:
(
Let us recall that we assume that our event structures are nite so that, in particular, we can de ne 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: 8e1 2 ran Gi: (
pi (e1) 2 Xi \ Gi 1! (fe1g) 8e0 2 Xi \ Gi 1! (fe1g) : t (pi (e1)) t (e0) : We have only one requirement to impose on p: 8e 2 ran Gi: s (e) t (p (e)) : This last requirement can be tightened to 8e 2 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 e cient ones. To make this kind of comparison more
precise, we introduce a measure to rank all the di erent 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 2 Xi \ (ran Gin dom Gi)
8e 2 Xi \ (ran Gin dom Gi) : t (zi)
t (e) :
(
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) =
[ e2Si Xi
b ( (e)) (y 2 [s (e) ; t (e)[):
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 lters 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 o , so that the range in that term is right-open). We nally ask the SMT solver to maximise maxift(zi)g
X where is a function returning the interaction between the labels denoted by l (t). 4
We have seen in Section 3.1 how the gap in expressiveness between standard
mathematical notation and the rst-order language of SMT solvers can cause
di culties when translating a mathematical problem for its computation in an
SMT setting. In some cases, reformulations are needed (recall how we passed from
(
Listing 1.1. SMT macro for (
The striking di erence between them is clearly a problem when examining the SMT code and in particular when this code needs to have some degree of con dence 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 e cient), 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 con dent 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 rst-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 de nitions 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 veri cation process. We now see a particular application of this general veri cation mechanism.
In Isabelle/HOL, we can introduce the following function: abbreviation " trueConcur01 ' G X lastParent startTime endTime == 8 child . ( X child & ( 9 parent . G parent child ) ) ! ( X ( lastParent child ) & ( G ( lastParent child ) child ) & ( 8 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 (
On the other hand, the Isabelle de nition 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 (
Max ( endTime ` ( X \ ( immediatePredecessors ' P f child g ) ) ) & 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 transitivere exive closure P (corresponding to ! ), and the in x operator ` takes the image of a set through a function. We note that the custom-de ned operator immediatePredecessors only makes sense for discrete relations; this is not a problem here, because we are in a nite 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 "f e2 2 X \ events P . e2 j ( 9 e0 2 X \ ( strict P )^ 1 ` `f e2 g .
startTime ( e2)<endTime ( e0 ))g=fg"
The thesis (introduced by the shows keyword) states that the set of the events
in X possibly admitting a predecessor ending after they start is empty (please
note that (strict P)^ 1 is the strict causality relation reversed, and ``{e2}
takes all the images of the singleton {e2} through it, thereby meaning all the
predecessors of e2 through P). Between the keywords assumes and shows there are
ve hypotheses. atomicTimeArrow formalises requirement (
To keep this generality, we had to prove several additional formal theorems about well-foundedness, some of independent interest. The following one, for example, is fundamental to the previous one, and states the intuitive idea that between two elements related by a well-founded order relation P, there must be a third one which is immediately related to one of them: lemma mm05ll : assumes " reflex P" " trans P" " antisym P" " wf ( strict P ) " " ( x , z ) in P" "z 6= x" shows "9 y . ( ( y , z ) 2 P & y 2 next1 P fx g ) " .
Here, next1 P {x} denotes the immediate successors of x according to the order relation P: the lemma states that for well-ordered relations, this function yields what is expected.
To recapitulate, our general approach to verifying SMT-LIB code proposes a chain of equivalent de nitions, with one end expressed in Isabelle/HOL and the other directly in SMT-LIB. Each of them is proven equivalent to the next either using the SMT solver or a formal Isabelle proof. At one point in the chain, we pass from an Isabelle de nition to an SMT-LIB one: here, we trust Sledgehammer to produce a rst-order SMT-LIB de nition from an Isabelle/HOL de nition restricted to the rst-order fragment of HOL.
This very last passage raises a key question: why should we trust Sledgehammer in building the formal proofs of our SMT-LIB code? After all, Isabelle itself does not trust Sledgehammer, but only uses its results to obtain guidance from various solvers, with the nal proof thus obtained re-checked for correctness inside Isabelle.
The answer starts from a basic observation: ultimately, veri cation is about reducing the amount of code to be trusted. Ideally, to a core small enough to be uncontroversial (see the de Bruijn criterion [2] which, nevertheless, implies trusting software/hardware below small core). But even reducing the trusted code from the extremely verbose SMT-LIB code to a limited amount of Sledgehammer's ML code is desirable, for various reasons. First, the latter stays the same when di erent SMT-LIB problems are considered. Second, possible soundness problems are linked to the fact that higher-order logic is much richer than SMT-LIB rst-order logic: in our approach, this issue is greatly mitigated by the fact that we use Sledgehammer translator for code (e.g., trueConcur01') which only uses a rst-order logic fragment of HOL, while the type-richer de nitions are con ned to duplicate Isabelle de nitions (e.g., trueConcur00') which are used for theorem proving and which are proved equivalent, within Isabelle, to the rst-order de nitions seen by the translator generating SMT code. Third, the limited portion of the SMT translator we need has had much more exposure and testing than any particular SMT-LIB code that we would need to trust without this approach. Fourth, ML (the functional, higher order language in which Isabelle and Sledgehammer are implemented) is arguably more readable than SMT-LIB. Fifth, contrary to the Isabelle case, we need to trust the SMT solver anyway because we are not using it to obtain proofs (which Isabelle can then reconstruct), but computations. And the size and complexity of the Sledgehammer implementation is vastly negligible in comparison. 5
We presented an SMT formulation for nding optimal true concurrent traces of execution. The typical issue of the SMT code getting rapidly unreadable is addressed by using a theorem prover to generate equivalent SMT assertions and then to prove correctness theorem about the latter. In previous work, we explored the problem of searching optimal traces of executions subject to linear interleaving. Here, we provided a novel approach to use an SMT solver for nding executions of optimal traces with a varying degree of concurrency. Future work could see the application of a similar approach to resource scheduling and optimisation problems.
This paper also contributes a way of characterising and computing a notion of degree of parallelism for arbitrary computations. Our de nition has some advantages over existing ones: contrary to [22], it does not require an empirical implementation on given hardware in order to analyse and compute the degree of parallelism of a given algorithm; it does not require to express the algorithm in a speci c language, as in [21]; it reduces to computing a numerical value through a simple procedure, rather than introducing de nitions (see functionals in Sections 1 and 2 of [21]) which are very useful for abstract analysis but, to the best of our knowledge, currently have no concrete implementation.
To make our work more useful, we plan to introduce additional metrics: besides the degree of concurrency, an user could nd useful to have further ways of comparing possible executions. For example, by considering how many events two possible solutions have in common, and what is their time distance.
We also plan to investigate possible connections between the SMT formalisation proposed here and other framework formalising concepts related to the ones emerging in this paper; for example, in Event Calculus [13], events and time are central.
Finally, we will continue exploiting the interplay between SMT solvers and theorem provers. As shown in the current and previous works, this interaction can be quite general and fertile. However, it has to be adapted on a case by case basis. This could be made easier by providing systematic, generic procedures to automate it at least in its most common use cases, for example the instantiation of a universal quanti er, which we faced in Section 4.