====== Modelling with Signal Transition Graphs: Distributed Mutual Exclusion ======

In the exercises below you will use //Signal Transition Graphs// (STG). STGs are Petri nets where actions (i.e. transition labels) have some extra semantics and short-hand drawing conventions are used:
  * The actions are partitioned into ''<color red>inputs</color>'', ''<color blue>outputs</color>'' and ''<color green>internal</color>''; there are also ''<color black>dummy</color>'' transitions that do not correspond to any actions and serve for the convenience of modelling, e.g. one can “hide” a redundant action by replacing its transitions with dummies without otherwise changing the behaviour of the system. Dummies are similar to ''ε'' in FSMs.
  * The actions have //directions//: ''+'', ''-'', or ''~''; e.g. ''a+'' means action ''a'' is asserted and ''a-'' means it is withdrawn. It is normally expected that transitions of ''a+'' and ''a-'' must alternate in every execution (this property is called [[help:verification|Consistency]]) – otherwise the model is ill-formed. The ''~'' is used for actions that do not have this assert/withdraw semantics, and by default ''~'' is not displayed at the end of the action name.
  * Short-hand drawing conventions are used:
    * Transition boxes are omitted – only labels (actions) are drawn.
    * Places with one incoming and one outgoing arc are normally not shown – transition-to-transition arcs are drawn instead (a token is put directly on such an arc if the original place is marked); this can be overridden for particular places if necessary.


===== Distributed Mutual Exclusion: Token Ring Architecture =====

The aim of the exercises below is to model a system that guarantees //Distributed Mutual Exclusion// (DME). There are N clients that should access a shared resource in a mutually exclusive way. To do that, N almost identical //DME elements// are connected in a ring. The first DME element is slightly different from the others in that it initially holds a “token” (do not confuse with Petri net tokens). This token is passed around the ring in the clockwise direction.

{{ circuit-dme.svg?50%,nolink |Distributed Mutual Exclusion (DME)}}

From time to time, a client may wish to use the shared resource. To do that, it requests permission from the corresponding DME element by asserting ''<color red>req</color>'': action ''<color red>req+</color>'' (note that from the point of view of the DME element this is an input, and so is shown in red). If the DME element does not hold the token, it has to wait for one. After the token has arrived (or if DME element has already been holding it), the DME element can grant the request to the client, by asserting ''<color blue>grant</color>'': output action ''<color blue>grant+</color>''. At this point the client knows that it is safe to enter the critical section and use the resource, as the other clients cannot be using it. Note that the DME element is not allowed to pass the token to the next DME element in the ring until the client notifies it (by withdrawing the request: action ''<color red>req-</color>'') that it has exited its critical section.

<WRAP center round tip 90%>
A request from the client may arrive when the DME element is about to pass the token to the next DME element in the ring. Hence, the DME element has a //choice//: it can either grant the request holding the token for longer or to pass the token and grant the request on the next round – either behaviour is acceptable. This choice expresses //arbitration//, as the DME element arbitrates between the client’s request and the decision to pass the token – which of them was first. If these events happened close in time, an arbitrary decision is made. If the system is to be implemented as a circuit, it will inevitably enter a metastable state from time to time, and so one has to use a //Synchroniser//, a //Mutual Exclusion element// or similar specialised circuitry that can handle metastability.
</WRAP>

Having finished using the resource, the client withdraws the request: input action ''<color red>req-</color>''. In response, the DME element withdraws the grant: output action ''<color blue>grant-</color>''. 

<WRAP center round tip 90%>
The sequence of events ''<color red>req+</color>'', ''<color blue>grant+</color>'', ''<color red>req-</color>'', ''<color blue>grant-</color>'' forms a so called 4-phase //handshake// – this is a very common mini-protocol in asynchronous systems.
</WRAP>

At this point the client is allowed to send another request, and the DME element is allowed either to pass the token to the next DME element in the ring or hold it for longer (and perhaps process another request from the client).

The advantage of this //Token Ring// architecture is that it can be implemented in a distributed way.

===== Exercise 1: Compositional Modelling =====
Model a DME system comprised of two DME elements. Start by creating STG models of two DME elements as shown below. These two models should be saved in separate files, and you could use copy-and-paste to reduce the amount of work. Note that the names of the actions are slightly different in these two STGs (to make them unique), and that the initial markings reflect that the first DME element holds the token while the second does not.

<WRAP>
<WRAP column half>
{{ dme1.svg?35%nolink |}}
</WRAP>
<WRAP column half>
{{ dme2.svg?35%nolink |}}
</WRAP>
</WRAP>

Directional actions (i.e. those with ''+'' or ''-'') are used to interface clients, whereas passing of the token between DME elements is modelled abstractly by undirected (i.e. ''~'') actions (these actions could be implemented by handshakes when the model is refined, but this is not required for this exercise). When place ''CS1'' or ''CS2'' is marked, the corresponding client executes its critical section. Note that short-hand notation is not used for these places, as they have special significance to the designer.

<WRAP center round tip 90%>
Note the choices between outputs, e.g. in the first DME element place ''token1'' is in the presets of ''<color blue>grant1+</color>'' and ''<color blue>move1to2</color>'' transitions. Such choices are usually due to //arbitration//, and lead to violation of [[help:verification|Output-persistence]] -- a circuit implementation would have to handle metastability, as explained above.
</WRAP>

These two DME elements communicate by executing shared actions ''moveXtoY''. Hence, the model of the overall system can be constructed compositionally, using the //parallel composition// operation. This functionality is accessible via the //Tools->Composition->Parallel composition [PComp]// menu. In the dialog window (see below) tick the names of the files to be composed, and select //Outputs / Make dummy//. The latter will turn the fused transitions into dummies, as they represent internal workings of the system. <wrap important>For this to work files //dme1.work// and //dme2.work// must be opened in the same instance of Workcraft.</wrap>

{{ parallel_composition_dialog-dme1_dme2.png?nolink |}}

The resulting STG model of the system should appear in a new tab. It is also shown below, after some manual editing to improve visual representation, in particular:
  * The layout was manually modified to resemble the layout of the original STGs.
  * Places ''CS1'', ''CS2'', ''notoken1'' and ''notoken2'' have one incoming and one outgoing arc, and so were not shown in the resulting composition. They can be made explicit by selecting the corresponding transition-to-transition arcs, clicking //Transformations->Make places explicit// and renaming.
  * The dummy transitions were renamed to correspond to the ''moveXtoY'' transitions in the original STGs.

{{ dme_composed.svg?35%,nolink |}}

===== Exercise 2: Simulation and Verification =====
Simulate your model. Try to re-create the following scenarios:
  * First client sends a request that is immediately granted, and then the handshake is completed. Check that the token cannot be passed to the next stage while the client is in its critical section.
  * Second client sends a request that cannot be immediately granted, as the corresponding DME element has no token yet. When the token arrives, the request is granted, and the handshake is completed.
  * First client sends a request, after which the system arbitrates between issuing a grant and passing the token to the next stage of the ring; the latter is chosen, and the request is granted after token arrives back to the first stage.
  * First client sends a request, but it is not granted even after several rounds, as the corresponding DME element keeps choosing to pass the token to the next stage.

Verify the following standard properties of the model:
  * Deadlock-freeness.
  * Consistency (i.e. for every ''a'', transitions of ''a+'' and ''a-''  alternate in every execution).

Verify the following custom properties of the model. Note that the tool checks if there is a reachable marking satisfying the provided Boolean expression. Hence, to check an //invariant// (i.e. a property that must hold in every reachable state of the system) you have to express its //negation// as a Boolean expression, and let the tool check that no reachable marking satisfies this expression. Do not forget to save the properties with appropriate names.
  * Mutual exclusion of places ''CS1'' and ''CS2''. Hint: ''<wrap spoiler>%%$P"CS1" & $P"CS2"%%</wrap>''.
  * At most one of the DME elements can hold the token. Hint: ''<wrap spoiler>%%$P"token1" & $P"token2"%%</wrap>''.
  * Places ''notoken1'' and ''notoken2'' are redundant and can be removed (together with their arcs) without affecting the behaviour of the system. A place is redundant if the absence of a token in it is never the sole reason of some transition being disabled. E.g. whenever there is a token on place ''token1'', there is always a token on ''notoken2'', and so transition ''move1to2'' is enabled, and also whenever there is no token on ''notoken2'' there is no token on ''token1'', and so ''notoken2'' is never the sole reason for ''move1to2'' being disabled. Hints:
    ** The redundancy of ''notoken1'': ''<wrap spoiler>%%$P"token2" & ~$P"notoken1"%%</wrap>''.
    ** The redundancy of ''notoken2'': ''<wrap spoiler>%%$P"token1" & ~$P"notoken2"%%</wrap>''.
    ** Since checking place redundancy is a common task, Worckraft supports it directly, either via a the pop-up menu accessible by right-clicking a place, or via selecting a place (or several places) and using the //Verification->Redundancy of selected places [MPSat]// menu. Note that if several places are selected, the property checks whether they all can be removed without changing the behaviour of the STG, i.e. it is different from each of the selected places being redundant in isolation: For example, two places may be duplicates of each other (i.e. have exactly the same connections and initial marking), so either of them is redundant and can be removed, but not both.
  * It is impossible for both grants to be asserted simultaneously (this property is violated). To check if an action is asserted use the construction ''%%$S"action"%%'', e.g. ''%%$S"grant1"%%''.  Hint: ''<wrap spoiler>%%$S"grant1" & $S"grant2"%%</wrap>''. Play the reported violation trace in the simulator and explain why mutual exclusion of places ''CS1'' and ''CS2'' holds in spite of this property being violated.
===== Exercise 3: Re-synthesis =====
As noted in the previous exercise, the STG has redundant places and can be simplified. Use //Conversion->Net synthesis [Petrify]// to obtain the following simplified STG (manual layout was used to make it look similar to the previous STG):

{{ dme_composed_simplified.svg?35%,nolink |}}

One can also contract the dummy transitions without changing the behaviour of the system, as they correspond to hidden internal actions – use the //Conversion->Dummy contraction [Petrify]// menu item. This completely hides the internal implementation of the system, as well as its distributed nature, leaving only its visible behaviour: The whole DME system is now abstracted to a single place controlling handshakes with the clients.

{{ dme_composed_resyn.svg?35%,nolink |}}

====== ======
{{page>:tutorial:feedback&inline}}