Structural Invariants for Parameterized Architectures
241
can only handle token-ring and pipeline topologies, but not trees; for these topologies
the verification reduces to checking satisfiability of a formula of WS1S. We have also
considered one example with tree-topology (see below), for which the formula was
constructed manually. Satisfiability of WS1S and WSκS formulae was checked using
version 1.4/17 of Mona [33]. We consider various examples separated in categories:
Cache Coherence. Following [24] we formalized and checked the described safety
properties and deadlock-freedom of the following cache coherence protocols: Illinois, Berkeley, Synapse, Firefly, MESI, MOESI, and Dragon.
Mutual Exclusion. We modelled and checked for deadlock-freedom and mutual exclusion Burns’ [35], Dijkstra’s and Szymanski’s [3] algorithms as well as a formulation of Dijkstra’s algorithm on a ring structure with token passing [30]. Furthermore, we check synchronization via a semaphore which is atomically aquired and
by broadcasting to ensure everyone else is not in the critical section.
Dining Philosophers. This is the classical problem of dining philosophers which all
take first the right fork and then the left fork. We consider the following “flavors”
of this problem:
– there is one philosopher who takes first her left and then her right fork,
– as above but the forks remember whom took them, and
– there are two global forks everyone grabs in the same order.
Preemptive Tasks. There are tasks which can be either waiting, ready, executing or
preempted. Initially one task is executing while all others are waiting. At any point
a task may become ready and any ready task may preempt the currently executing
task. Upon finishing the executing task re-enables one preempted task. Here, we
have additionally two alternatives: Firstly, we consider the case where always the
agent with highest index resumes execution. Secondly, we let the processes establish the initial condition from a position where everyone is waiting (referenced later
as uninitialized).
Dijkstra-Scholten. This is an algorithm that is used to detect termination of distributed
systems by message passing along a tree [25]. Since the prototype only supports
linear topologies we can generate the necessary formula automatically only for this
case.
Herman. This algorithm implements self-stabilizing token passing in rings. The formulation is modelled after [19]. This applies for all following examples. Hence, we
describe the examples only in little detail.
Israeli-Jalfon. This is another self-stabilizing token passing algorithm in rings.
Lehmann-Rabin. This is a randomized solution to the dining philosophers problem.
Dining Cryptographers. A group of cryptographers want to determine if one of them
paid for a meal or a stranger but do not reveal how they acted individually.
The results are shown in Table 1. The first column reports the size of the example
in terms of the amount of states (#st.) and clauses (#cls.). The second column indicates
which properties could () and could not be verified (×) because the conjunction of
trap and one-invariant was not strong enough to prove the given property. The third
column reports the time (in second) it takes to prove all considered properties. These
results are measured on the provided virtual machine for artifacts [32] where the host
system is an average laptop. To understand the next four columns, recall that Mona
241
can only handle token-ring and pipeline topologies, but not trees; for these topologies
the verification reduces to checking satisfiability of a formula of WS1S. We have also
considered one example with tree-topology (see below), for which the formula was
constructed manually. Satisfiability of WS1S and WSκS formulae was checked using
version 1.4/17 of Mona [33]. We consider various examples separated in categories:
Cache Coherence. Following [24] we formalized and checked the described safety
properties and deadlock-freedom of the following cache coherence protocols: Illinois, Berkeley, Synapse, Firefly, MESI, MOESI, and Dragon.
Mutual Exclusion. We modelled and checked for deadlock-freedom and mutual exclusion Burns’ [35], Dijkstra’s and Szymanski’s [3] algorithms as well as a formulation of Dijkstra’s algorithm on a ring structure with token passing [30]. Furthermore, we check synchronization via a semaphore which is atomically aquired and
by broadcasting to ensure everyone else is not in the critical section.
Dining Philosophers. This is the classical problem of dining philosophers which all
take first the right fork and then the left fork. We consider the following “flavors”
of this problem:
– there is one philosopher who takes first her left and then her right fork,
– as above but the forks remember whom took them, and
– there are two global forks everyone grabs in the same order.
Preemptive Tasks. There are tasks which can be either waiting, ready, executing or
preempted. Initially one task is executing while all others are waiting. At any point
a task may become ready and any ready task may preempt the currently executing
task. Upon finishing the executing task re-enables one preempted task. Here, we
have additionally two alternatives: Firstly, we consider the case where always the
agent with highest index resumes execution. Secondly, we let the processes establish the initial condition from a position where everyone is waiting (referenced later
as uninitialized).
Dijkstra-Scholten. This is an algorithm that is used to detect termination of distributed
systems by message passing along a tree [25]. Since the prototype only supports
linear topologies we can generate the necessary formula automatically only for this
case.
Herman. This algorithm implements self-stabilizing token passing in rings. The formulation is modelled after [19]. This applies for all following examples. Hence, we
describe the examples only in little detail.
Israeli-Jalfon. This is another self-stabilizing token passing algorithm in rings.
Lehmann-Rabin. This is a randomized solution to the dining philosophers problem.
Dining Cryptographers. A group of cryptographers want to determine if one of them
paid for a meal or a stranger but do not reveal how they acted individually.
The results are shown in Table 1. The first column reports the size of the example
in terms of the amount of states (#st.) and clauses (#cls.). The second column indicates
which properties could () and could not be verified (×) because the conjunction of
trap and one-invariant was not strong enough to prove the given property. The third
column reports the time (in second) it takes to prove all considered properties. These
results are measured on the provided virtual machine for artifacts [32] where the host
system is an average laptop. To understand the next four columns, recall that Mona