description and generation of correct implementation code. We illustrate our idea by applying the technique to a parallel implementation of explicit state-space exploration.
Parallel and distributed computing address important problems of scalability
in computer science, where some problems are too large or complex to be
handled by just one computer. Until now, focus has mostly been on distributed
algorithms, i.e., algorithms running on multiple computers communicating via a
network, as access to parallel computers, i.e., computers capable of running
multiple processes communicating via shared memory (RAM), has been limited. For
this reason, there are many papers on modeling distributed algorithms, such as
network protocols [
Classically, formal models can partake in a development in two different
ways: by extracting an implementation from a model, which we call model-driven
software engineering, or by extracting a model from an implementation, which
we call model-extraction . Our focus in this paper is on model-extraction but
in a way that allows us to also do code generation, thereby allowing a new
combined approach. The model-driven engineering approach is shown in Fig. 1
(top) and shows that we start with model which is verified according to one or
more properties. If it is ok, we can extract a program, and otherwise we refine the
model. Examples of this approach are within hardware synthesis [
The model-driven software engineering and model-extracti on approaches have different strengths and weaknesses. The main strength of the model-driven softUNIT Fig. 1: Model-driven software engineering (top) and model- extraction (bottom).
COUNTER_EXAMPLE MODEL
m ware engineering approach is that it is possible to verify an algorithm before implementation and we can even get a guaranteed-correct (te mplate) implementation with little or no user-interaction. The disadvantag e is that the approach is of little use for already existing software. The model-ex traction approach precisely alleviates this by extracting a model from an existing implementation automatically, ensuring there is correspondence between the model and implementation. The main disadvantage is that we need an implementation of a, perhaps faulty, algorithm before analysis can start.
We would like to provide a translation supplying as many of the strengths of these approaches as possible. By supporting model-extra ction in a way that allows subsequent code generation, we can support both approaches plus a new merged approach, shown in Fig. 2. Here we extract a model from a description in one – possibly abstract – language, manually or autom atically refine the abstraction until we can prove the system to be correct (optionally modifying the original description if we find errors), and then extract an implementation. While the last step seems superfluous if we already have an implementation, it can be useful, for example, to use a program written in pseudo-code as input, automatically derive and verify a model, and from the model extract a runnable program in a desired implementation language. Alternatively, we can do roundtrip engineering, where we take an implementation as input, verify and correct it on the level of a model, and update the original implementation to reflect the changes.
To do this, we use systematic extraction and abstraction methods that can
be derived from a program or from an algorithm written in pseudo code. Our
approach builds on process-partitioned coloured Petri nets (PP-CPNs) as
described in [
1
PROGRAM p p' 1`ininititiaial_l_aabbssttrraaccttioionn
1 initial_abstraction Refine Program c
Model Extraction a a
Refine Abstraction m () p ABSTRACTION
MODEL replaying errors found in an abstract model on the original program and using about why a given error-trace cannot be replayed in the origi nal program to refine the abstraction.
In this paper we focus on model-extraction. Our goal is to pro vide a
proofof-concept, so we do certain steps that can be automated by ha nd, such as the
translation from code to a model using patterns. We do not address refinement
after discovery of errors in this paper, but assume an external library using
CEGAR or a user takes care of that. We have already treated the code generation
aspect in [
The rest of this paper is structured as follows: in the next section, we
introduce process-partitioned coloured Petri nets as defined in [
In this section, we briefly introduce process-partitioned C PNs as defined in [
Process-partitioned CPNs. Coloured Petri nets (CPNs) consist of places, transitions, and arcs. Places are typed and arcs have expressions that may contain variables. Places may contain tokens and we call the distribution of tokens on all places a marking of the net, and the marking before executing any transitions the initial marking. CPNs have a module concept, where subpages are represented by substitution transitions.
In [
In the initial marking, exactly one of the process places must contain all tokens of the process colour set and the remaining process places must be empty (modeling that all processes must start in the same location in the program). Local places must initially contain exactly one token for each process so that if we project onto the component of the process colour set, we obtain exactly one copy of all values of the set (modeling that all local variables must be initialized). All shared places must contain exactly one value (modeling that shared variables must be initialized). All arc expression must ensure that tokens are preserved.
We have chosen to adopt the notion that we cannot create new processes
or destroy processes from [
Approach 1: Waiting ← { Model.initial()} 2: Visited ← { Model.initial()} 3: while Waiting 6= ∅ do 4: Pick a s ∈ Waiting 5: Waiting ← Waiting \ { s} 6: // Do any handling of s here 7: for all b enabled in s do 8: Execute b in s to get s′ 9: if s′ ∈/ Visited then 10: Waiting ← Waiting∪{ s′ } 11: Visited ← Visited ∪ { s′ }
We introduce our approach to verifying parallel algorithms by a parallel version
of the algorithm for generating state-spaces shown in Fig. 3 . The basic idea is
to use the loop of Fig. 3 for each process and share the use of Waiting and
Visited, naturally with appropriate locking. From this algorithm, we illustrate
our approach to extract a PP-CPN model. The last step, going f rom a PP-CPN
model to implementation code, is handled in [
A simple way to parallelize Fig. 3 is shown in Fig. 4 (left). Here, we initialize as before (ll. 1–2). We have moved the main loop to a separa te procedure, computeStateSpace. We perform mostly the same loop as before (ll. 16–24), but instead of testing for emptiness and picking an element of the queue in three steps, we do so using a procedure pickAndRemoveElement (ll. 17 and 24). The implementation of pickAndRemoveElement (ll. 4–9) does the same as we did before, except we return a bottom element ⊥ if no elements are available and use that in the condition of the loop (l. 18). This forces us to perform the pick in two places: before the first invocation of the loop (l. 17) and at the end of the loop (l. 24). Handling of states (l. 19) and iteration over all enabled bindings (ll. 20–21) is the same as before. Now, instead of checki ng if a state is a member of Visited and conditionally adding it to the set, we do both in a single step as shown in the procedure addCheckExists (ll. 22 and 11–14). We do this under the assumption that adding an element to the set does nothing if the element is already there. If the state was not already in Visited, we add it to Waiting (l. 23). The reason for this re-organization is that we now as sume that pickAndRemoveElement, addCheckExists, and the access to Waiting in line 23 are atomic, e.g., by creating a data-structure ensuring t his or by requesting a lock for each data-structure before the start of an operatio n and releasing it afterward. This allows us to start two instances of computeStateSpace in parallel in lines 26–27. We will not argue for the correctness of neith er Fig. 3 nor Fig. 4 (left), but note that it is easy to convince ourselves that if one is correct, so is the other with the assumption that pickAndRemoveElement and addCheckExists happen atomically.
Model Extraction. To go from Fig. 4 (left) to a PP-CPN model, we first extract the control-flow of the algorithm including generat ing representations of data, and then we refine the update of the data until we can prove the properties of the model we want.
Extracting the control-flow consists of creating the proces s places and
transitions of the model. We do that using templates, very similar to the
workflowpatterns [
In the initial abstraction, we translate a condition to an unbound boolean variable in the PP-CPN model. We add a local place for each loc al variable and a shared place for each global variable. These are available on all subpages where they are within the scope. In the initial abstraction, we approximate the type 1: Waiting ← { Model.initial()} 2: Visited ← { Model.initial()} 3: 4: proc pickAndRemoveElement() is 5: if Waiting = ∅ then 6: return ⊥ 7: Pick a s ∈ Waiting 8: Waiting ← Waiting \ { s} 9: return s 10: 11: proc addCheckExists(s′ ) is 12: result ← s′ ∈/ Visited 13: Visited ← Visited ∪ { s′ } 14: return result 15: 16: proc computeStateSpace() is 17: s ← pickAndRemoveElement() 18: while s 6= ⊥ do 19: // Handle s here 20: for all b enabled in s do 21: Execute b in s to get s′ 22: if addCheckExists(s′ ) then 23: Waiting ← Waiting ∪ { s′ } 24: s ← pickAndRemoveElement() 25: 26: computeStateSpace() 27: | computeStateSpace() 1: Waiting ← { Model.initial()} 2: Visited ← { Model.initial()} 3: MayAdd ← 0 4: 5: proc pickW ithCounter() is 6: s ← pickAndRemoveElement() 7: if s 6= ⊥ then 8: MayAdd ← MayAdd + 1 9: return s 10: 11: proc computeStateSpace() is 12: repeat 13: s ← pickW ithCounter() 14: while s 6= ⊥ do 15: // Do any handling of s here 16: for all b enabled in s do 17: Execute b in s to get s′ 18: if addCheckExists(s′ ) then 19: Waiting ← Waiting ∪
{ s′ } MayAdd ← MayAdd − 1 s ← pickW ithCounter() until MayAdd=0 20: 21: 22: 23: 24: computeStateSpace() 25: | computeStateSpace() of all variables with UNIT, and local and shared places are not connected to transitions.
Applying this extraction to the computeStateSpace procedure of Fig. 4 (left) and flattening it, we obtain Fig. 6 (left). Transitions are named after the line number they correspond to and conditions after the performed tests. Assign To Value stems from expanding the for all loop in line 18 to a while loop and line 19 has been omitted. We have instantiated the process twice (initial marking of S). Abstraction Refinement. The initial abstraction allows execution of traces not allowed in the original program. In the model in Fig. 6 (left), it is possible to first terminate p(1) and have p(2) continue computation. This is not possible in Fig. 4 (left). The model does find all possible interleavings of the process, though, so if the state-space does not contain any erroneous states, neither will the program.
Abstraction refinement consists of using more elaborate types on local and shared places, of adding arcs for reading and updating local and shared places,
S pIind P Atomic pid
E Out P
S pIind P
S1 S1 pid pid P
S2 S2 pid
E Out P if condition then 1`pid else empty pid P
pid
S pIind P
If
E Out P if condition then empty else 1`pid pid
P pid ElseS2
S pInid P
While if condition then 1`pid else empty pid pid P
S S if condition then empty else 1`pid
E Out P
Mutex 1 1t`rtureue pid P
S BOOL
S true false false true
S pInid P Acquire pid pid pid P Release pid
E Out P and of limiting the values of condition variables, often using values from the local or shared places. Refinements must limit the behavior of previous models (which formally must be able to simulate any refinement if we ignore local and shared places), and must be true to the original program.
The basic idea is to refine the types of places modeling local and global variables and add tests accordingly. When we cannot determine an exact test or update, we solve it by non-deterministically choosing amon g the possible values. Here we only do a simple refinement to avoid the situation where one process can decide that Waiting is empty just to have the other immediately afterward decide it is not. For this, we refine the type of Waiting to a BOOL, indicating whether the Waiting set is empty or not, and refine the type of s to indicate whether ⊥ was returned from isEmpty. The value of Waiting is initially false (as we add the initial state in line 1 of Fig. 4 (left)) and we do not care about the initial value of s, as it will be set before it is read. We make sure to read and update the values of Waiting and s faithfully. Adding an element to Waiting (l. 23) implies setting the value to true and for picking elements (ll. 17 and 24), we read the previous value of Waiting, use that to set the value of s, and non-deterministically set the value of the waiting set to true or false (though if the value already was true it remains so) as we do not have enough information to know which is the correct answer. We obtain the model in Fig. 6 (right). For readability, we have merged the transitions 17 and 24, but this is not necessary for analysis. We no longer can execute the erroneous trace on this refined model. 4
The main reason we started this work in the first place is to analyze parallel algorithms. Our focus is on new problems arising when creating parallel algorithms, not on proving correctness of serial algorithms. We therefore assume that pidS P2 11``Ppp.((a12l))l(+)+
17 pid pid P pid
24 pid
if waitingNonEmpty
if waitingNonEmpty tehlseene1m`ppitdy E if moreEnabledBindingspid P P then empty else 1`pid
While 20 P if moreEnabledBindings then 1`pid else empty pid algorithms are correct under certain mutual-exclusion ass umptions, and search for such violations. We are also interested in potential dead- and live-locks. Assuming a valid refinement, we can ensure that absence of safety violations in the model guarantees absence in the real program as we can simulate all executions of the algorithm. This includes proving absence of mutual-e xclusion violations. We cannot use our approach to ensure the absence of dead-lock s, as we deal with over-approximations of the possible interleavings an d further restricting the behavior may introduce new dead-locks, but we can still fi nd dead-locks and remove them from the implementation.
We can do state-space analysis of the derived models from Fig . 6, and obtain a state-space with 81 states for the abstract model (left) an d a state-space with 130 states for the refined model. As the models do not have any critical regions, they of course have no mutual exclusion violations. Dead-locks and Live-locks. As all processes have a distinguished start and end-state, we can recognize dead-locks and live-locks in th e model. A dead-lock is a state without successors (a dead state) where not all processes reside on E. Neither of the models in Fig. 6 has dead-locks; the model to th e left has exactly one dead state, where all process ids reside on E and the shared and local places retain their initial marking. The model in Fig. 6 (right) also has one dead state, where all process ids reside on E, Waiting is true, s is true for all processes, and all remaining local and shared places have their initial value.
Live-locks are a harder to recognize. We only consider live- locks in the absence of dead-locks. A model has a strong live-lock if the dead states of the model do not constitute a home space, i.e., if it is not always possible to reach one of the dead states. A strong live-lock in the model does not necessa rily imply a livelock in the original algorithm, but can be used to identify parts of the original program that should be further investigated. None of the models in Fig. 6 have strong live-locks.
A model may have a weak live-lock if its state-space has a loop. A loop may also just indicate that a loop may execute an unbounded number of times. Both models in Fig. 6 have loops, but analysis shows that the transition While 20 is impartial , i.e., that in any infinite execution it occurs an infinite number of times. This happens if we compute infinitely many successors (the state-space has infinitely many states), and makes sense in our algorithm.
A particular interesting kind of live-lock is a loop reachab le from a state where E contains tokens. This means that even after one of the processes have terminated, the amount of work done by another process is unbounded. We have already seen that Fig. 6 (left) exhibits this due to too abstract modeling, i.e., that process p(1) may decide that Waiting is empty initially and terminate, just to have p(2) decide it is non-empty and continue computation. We have see n this is not possible in the original algorithm, which caused us to refine the model to Fig. 6 (right). We would therefore expect that no such live-l ock was present in the refined model. Maybe surprisingly, one such does exist. This is seen by having p(1) check Waiting in 17/24, modify Waiting to be empty, and successfully continue. Then, p(2) checks Waiting, notices it is empty and terminates. Now, p(1) continues. This is also possible in Algorithm 4 (left), and even quite likely as the two processes will test Waiting initially, one of them will consume the only element it contains initially, and other processes terminate. This also occurred in reality in our first implementation of a parallel state-spac e exploration algorithm using Algorithm 4 (left).
To fix this, we notice that the reason p(2) terminates prematurely in the previous example is that it decided to terminate while p(1) can still add new states to Waiting. The idea of an improved algorithm is to ensure that no processes may terminate when others may produce new states. This prompts us to make Algorithm 4 (right). We reuse calculateStateSpace, addCheckExists, and pickAndRemoveElement from Algorithm 4 (left) and define a new procedure for picking, pickW ithCounter (ll. 5–9) which is used in place of the original pickAndRemoveElement (ll. 13 and 21). We use MayAdd as a counter of the number of processes which may add new states to Waiting. We add an additional loop around the previous main loop ensuring we only quit when MayAdd is zero. We inline the call to pickW ithCounter for the translation and use a mutex around the call to ensure atomicity.
We use the same approach to translate the model to a CPN model. We maintain the abstraction of Waiting and do no abstraction of MayAdd, i.e., we increment and decrement it according to the algorithm. We implement the mutex around the call to pickW ithCounter as a place with type UNIT containing a single token acting as the mutex. We then obtain the model in Fig. 7. We have not completely flattened it for readability and to keep resemblance with the previous models in Fig. 6. At the left we have the loop in lines 13–21, which mostly corresponds to Fig. 6 (right). The only changes are that aside from renaming transitions to correspond with the line numbers of Algorithm 4 (right), we have added a transition for the new line 20 causing some rerouting of the flow, added a place representing MayAdd, and changed 13/21 (named 17/24 in Fig. 6) to a substitution transition. We have modeled the new outer loop as a separate page shown in Fig. 7 (top/right). We implement the semantics of a repeat/until loop looping over the page in Fig. 7 (left). We share access to MayAdd. The Test transition is explained later. The page corresponding to the substitution transition modeling pickW ithCounter is shown in Fig. 7 (bottom/right). Again, we share access to a local place (s) and two shared places (MayAdd and Waiting). In all cases, the S and E places of a subpage is in port/socket relationship with the input and output place of the corresponding substitution transition.
We can use state-space analysis to verify that (for this confi guration) we do not violate the mutex property in pickW ithCounter. The state-space for this model contains 399 states and 934 bindings. We can check this explicitly by looking at the total number of tokens on the four unnamed places in Fig. 7 (bottom/right). This is either 0 or 1, showing that never do we have more than one process inside pickW ithCounter. The Test transition in Fig. 7 is added to easily test whether it is ever possible for a process to execute lines 15–20 while another process has terminated, i.e., whether it is possible for a process to terminate while there is still work to do. The transition requires a token from E, i.e., a process that terminated and that the value of MayAdd is non-zero (this is handled by the guard [n<>0], which has not been explained but exactly ensures this). If Test is enabled in any state, it means that a process has terminated while another has more work to do. State-space analysis shows this is not the case. This is also a safety property, so absence of violations in the model implies absence of violations in the original algorithm. We can prove the property without adding Test by searching for a state where E has tokens and Waiting is false or one of the unnamed places below While 14 contains tokens.
We can convince ourselves that the mutex around pickWithCounter is necessary by removing it and repeating analysis. We then get a state where Test is enabled, and we can verify the same error is present in the original model (have one process enter pickW ithCounter and consume the last element of Waiting,
S 2 11``Ppp.((a12l))l(+)+ pIind P 13/p2i1ck pid pid P if isNotBottom(s)
then empty
(pid, s) if isNotBottom(s) then 1`pid else empty pid P
While 16 if moreEnabledBindings then 1`pid else empty then have the other process enter pickW ithCounter, notice there is no element and return ⊥, and terminate, just to have the first process continue alone).
In addition to the analysis of non-termination, we naturall y also check for dead- and live-locks as before and find nothing unexpected. W hile Algorithm 4 (left) is quite simple and it is probably possible to convince oneself that it is correct without verification, the introduction of MayAdd makes Algorithm 4 (right) sufficiently complicated that correctness is not immediately apparent. We have verified the algorithm with up to 4 processes (yielding 55.709 states), which is the configuration we use in practice. Verification has given us confidence that the algorithm will work with any number of processes. We have also investigated an extended version additionally adding a checkpointing mechanism where all threads are paused while Waiting and Visited are written to disk in a consistent configuration.
We also used the method to verify the implementation of a slightly simplified
version of the protocol for operational support developed in [
We have sketched an approach for correct implementation of parallel algorithms.
The approach allows users to extract a model from an algorithm written in an
implementation or abstract language and verify correctness using state-space
analysis. The approach also facilitates the generation of skeleton implementation
code from the verified model using the approach from [
Verification of software by means of models is not new. Code-g eneration
from models have been used in numerous projects. The approach has been
most successful for generating specification of hardware from low-level Petri
nets and other formalisms to synthesize hardware such as computer chips [
The work presented here is only in the initial stages, but looks very promising. We have several ideas for future work. Currently, we have to manually extract the model from patterns. This is tedious and error-prone, an d it would be nice to have automatic extraction. Such a translation should implement the patterns included in Fig. 5, but could also use explicit patterns for repeat/until loops and other constructs. Given an implementation of the translation to and from models, we could look at supporting a full development cycle allowing us to update existing code with changes to the model.
An implementation could also implement reduction rules like the one we used to merge lines 17 and 24 in the model in Fig. 6 (right). We can also add simplifications collapsing long traces of unconditional progress not modifying any data to reduce the state-space without removing behavio r. For example, in Fig. 7 we can remove transitions Assign To Value and 17, merging the input place of Assign To Value and the output place of 17, to obtain a smaller state-space of 26.909 states for 4 processes, down from 55.709 states. We can also merge the acquisition of a lock with the first regular transition (merging the transitions Acquire Lock with 6 in Fig. 7 (bottom/right)) and merging releases with the last. This reduces the state-space to 14.841 states.
Currently, we provide abstractions manually. Like SLAM, we could easily replay found errors on the original code and provide assistance in the development of refinements, possibly even making them automatically. In our example, replaying the early termination error trace found in Fig. 6 (left) on Algorithm 4 (left) would show that it is not possible for isEmpty to return false initially and that it can only change from returning false to returning true if we execute line 23. Even though we might not be able to provide the abstraction refinement in Fig. 6 (right) fully automatically, providing such diagnostics can be very useful for the user for improving the refinement.
Our current method focuses on parallel algorithms with a fixed number of
identical processes, but there is nothing in our approach preventing us from
extending this to also handle distributed settings with asynchronous
communication using buffer places and different kinds of processes; the code generation
in [
One thing our approach does not support very well at the moment is intraprocedure calls. We can currently simulate this in simple cases by inlining procedure calls, but this is not possible when using recursion. One way to fix it is to view a recursive call as starting a new process for executing the child and waiting for the result. If we support different kinds of processes, communication between processes, and dynamic instantiation of processes, this should be easy to add.