Model-Checking
CS511
1/76
Program Correctness
Model-Checking
Introduction to Promela
Assertion Based Model Checking Turnstile Example
MEP
End States
2/76
Program Correctness
Main approaches to demonstrating that a program does what it’s supposed to do:
1. Testing
2. Deductive verification 3. Model-checking
3/76
Testing
Fast and simple way to detect errors
Can never be sure there are no defects (cannot cover all the cases) – maybe tests weren’t comprehensive enough
Testing shows the presence, not the absence of bugs1
Testing Concurrent Programs
More difficult since we would like to test all interleavings
But since interleaving is controlled by OS scheduler, user cannot arrange arbitrary interleavings
Consequence: very few of possible interleavings are tested
1Dijkstra (1969) J.N. Buxton and B. Randell, eds, Software Engineering Techniques, April 1970, p. 16. Report on a conference sponsored by the NATO Science Committee, Rome, Italy, 27–31 October 1969.
4/76
Proving Programs Correct
Holy Grail of computer science
Using special specification language, describe
1. State of program’s variables
2. How each programming language statement uses variables
Specification language is mixture of mathematics & programming language
5/76
How to Prove a Program Correct
Hoare Triples
P program
A precondition B postcondition
AP B
A and B are predicate logic formulae over an extended first-order language
6/76
Example
y:=1;
z:=0;
while (z!= x) {
z:=z+1;
y:=y*z }
1 2 3 4 5 6
Assertion
Using hoare triples: TruePy = z! ∧ z = x
In prose: Under any state σ, if P terminates in a state ρ, then ρ satisfies y = z! ∧ z = x
Provable Assertion
Prove TruePy = z! ∧ z = x in some deductive proof system
7/76
Sample Deductive Proof System for Partial Correctness
AC1B BC2C
AC1 ; C2 C (Composition)
A{x/E}x := EA (Assignment) A ∧ BC1D A ∧ ¬BC2D
Aif B then {C1} else {C2}D (Conditional)
A → A′ A′PB′ B′ → B AP B
(Implication)
A ∧ BCA
Awhile B {C }A ∧ ¬B (While-Partial)
8/76
Example of Partial Correctness Proof
Ty := 1;z := 0;while(z! = x){z := z +1;y := y ∗z}y = z!∧z = x
y ∗ (z + 1) = (z + 1)!z := z + 1y ∗ z = z!
y = z! ∧ z ̸= xz := z + 1y ∗ z = z! y ∗ z = z!y := y ∗ zy = z!
y = z ! ∧ z ̸= x z := z + 1; y := y ∗ z y = z ! y = z!Qy = z! ∧ z = x
Q = while (z ! = x ) {z := z + 1; y := y ∗ z }.
1=0!y :=1y =0! y =0!z :=0y =z!
Ty :=1;z :=0;y =z! y =z!Py =z!∧z =x
Ty :=1;z :=0;Py =z!∧z =x
9/76
Drawbacks of Program Proof
Proving that arbitrary program X has property Y is undecidable
Precisely specifying all of program’s intended actions is notoriously hard
Doing such a detailed spec & associated proofs usually much harder than writing & testing the program!
Dynamic memory management (heap) is difficult to reason about
Concurrency is even more difficult to reason about
See well-known books by Manna and Pnueli (1992,1995) or text by Apt et al (2009)
10/76
Research in Program Proof is Active
Deductive verification is still too complicated for realistic programs/languages
But it is growing fast!
The Atelier B system was used to develop part of the
embedded software of the Paris metro line 14 and other
railroad-related systems
Formally proved C compiler was developed using the Coq proof
assistant (http://compcert.inria.fr)
Microsoft’s hypervisor for highly secure virtualization was
verified using VCC and the Z3 prover
L4-verified project developed a formally verified micro-kernel
with high security guarantees, using analysis tools on top of
the Isabelle/HOL proof assistant (https://sel4.systems)
https://deepspec.org/main
11/76
Program Correctness
Model-Checking
Introduction to Promela
Assertion Based Model Checking Turnstile Example
MEP
End States
12/76
Model-Checking
1. Develop a model of the program
This helps abstract away from unnecessary details
Provides a different way of thinking about your problem Must be careful to not oversimplify
2. Prove properties of the model
Use tools to analyze the model
Code
Model
Property
Model checker
Overflow
Yes
No Counter-example
13/76
Software Model Checking
Software model checking is the algorithmic analysis of programs to prove properties of their executions
There is an extensive literature on this topic
We only focus on one example (explicit state, automated, model-checking for temporal logic based on automata techniques)
Survey:
Ranjit Jhala, Rupak Majumdar: Software model checking. ACM Comput. Surv. 41(4): 21:1-21:54 (2009)
14/76
Model-Checking
Two well-known explicit-state model-checkers for concurrent/distributed computing
Spin (we’ll use this one)
Developed by Gerard Holzmann (1980s)
Awarded ACM’s Software System Award in 2001
Example of use:
Mars Code, Gerard J. Holzmann, Communications of the ACM, Vol. 57 No. 2, Pages 64-73, Feb 2014
TLA+
Developed by Leslie Lamport (1994)
Example of use:
How Amazon Web Services Uses Formal Methods, Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff, Communications of the ACM, Vol. 58 No. 4, Pages 66-73, April 2015
15/76
Promela
Spin uses Promela (PROcess MEta LAnguage) for representing models
The aim of Promela is to model concurrent and distributed systems
We’ll look at some examples of Promela code
They can be executed using spin
16/76
Bibliography
Tutorial on Promela:
Model Checking Concurrent Programs, Ian Barland, Moshe Vardi and John Greiner. Available here: https://cnx.org (search for title above)
Principles of the Spin Model Checker, Mordechai Ben-Ari, Springer-Verlag London, 2008.
17/76
Model-Checking: Plan
1. Introduction to Promela
2. Assertion based model checking 3. LTL based model checking
18/76
Program Correctness Model-Checking Introduction to Promela
Assertion Based Model Checking Turnstile Example
MEP
End States
19/76
Promela Models
Consist of:
type declarations
channel declarations variable declarations process declarations init process
mtype = {MSG, ACK}; chan toS = …
chan toR = …
bool flag;
proctype Sender() {
… process body …
}
proctype Receiver() { …
}
init { …
}
1 2 3 4 5 6 7 8 9
10
11 no unbounded data 12
Corresponds to a (usually large, but) finite transition system, so
no unbounded channels
13
14
no unbounded processes 15
no unbounded process creation
16
20/76
Simple Sequential Program (eg1.pml)
active proctype P() { byte N = 10;
byte sum = 0;
byte i;
for (i : 1 .. N) { sum = sum +i;
}
printf(“The sum of the first %d numbers = %d\n”,
}
N, sum);
1 2 3 4 5 6 7 8 9
10
P is referred to as the process type active spawns a process type
21/76
Simple Sequential Program
active proctype P() { byte N = 10;
byte sum = 0;
byte i=1;
do
:: i > N -> break :: else ->
sum = sum + i; i++
od;
printf(“The sum of the first %d numbers = %d\n”,
}
N, sum);
1 2 3 4 5 6 7 8 9
10 11 12 13
Same as previous example only uses do-od
22/76
Simple Interleaving (eg2.pml)
byte n = 0;
active proctype P() { n = 1;
printf(“Process P, n = %d\n”, n); }
active proctype Q() { n = 2;
printf(“Process Q, n = %d\n”, n); }
1 2 3 4 5 6 7 8 9
10 11
23/76
Simple Interleaving with Race Condition (eg3.pml)
byte n = 0;
active proctype P() { byte temp;
temp = n + 1;
n = temp;
printf(“Process P, n = %d\n”, n)
}
active proctype Q() { byte temp;
temp = n + 1;
n = temp;
printf(“Process Q, n = %d\n”, n)
}
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15
Statements are atomic in Promela; interleaving occurs in an if- or do-statement (more later)
24/76
Simple Interleaving with Race Condition (eg4.pml) Same as previous example but shorter
Note the use of [2] and _pid (predefined variables start with an underscore)
byte n = 0;
active [2] proctype P() { byte temp;
temp = n + 1;
n = temp;
printf(“Process P%d, n = %d\n”, _pid, n);
}
1 2 3 4 5 6 7 8
25/76
Simple Interleaving with Race Condition (eg5.pml)
init is the first process that is activated
run instantiates a process
Convention: run expressions are enclosed in atomic so that all
processes are instantiated before any of them begins execution
byte n;
proctype P(byte id; byte incr) { byte temp;
temp = n + incr;
n = temp;
printf(“Process P%d, n = %d\n”, id, n) }
init {
n = 1;
atomic {
run P(1, 10); run P(2, 15)
} }
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16
26/76
Simple Interleaving with Race Condition (eg6.pml)
The body of a process consists of a sequence of statements. A statement is either
executable: the statement can be executed immediately. blocked: the statement cannot be executed.
An assignment is always executable.
An expression is also a statement; it is executable if it evaluates to non-zero.
2 < 3 x < 27 3 + x
always executable
only executable if value of x is smaller 27 executable if x is not equal to –3
27/76
Simple Interleaving with Race Condition (eg6.pml)
(_nr_pr == 1) causes init to block until the expression is true (_nr_pr is number of processes currently running)
byte n = 0;
proctype P() { byte temp, i;
for (i:1..10) { temp = n;
n=temp+1
} }
init { atomic {
run P(); run P()
}
(_nr_pr == 1);
printf("The value is %d\n", n); }
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16
28/76
Program Correctness Model-Checking Introduction to Promela
Assertion Based Model Checking Turnstile Example
MEP
End States
29/76
Assert (eg8.pml)
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16 17 18
1 2 3
30/76
byte n = 0;
byte finished = 0;
active [2] proctype P() { byte i = 1;
byte temp;
for (i:1..10) {
temp = n;
n = temp + 1 }
finished ++; /* Process terminates */ }
active proctype Finish() {
finished == 2; /* Wait for termination */ printf("n = %d\n", n);
assert (n > 2); /* Assert can’t be 2 */
}
$ spin -a eg8.pml $ gcc -o pan pan.c $ ./pan
Verification in Spin using assert
Spin reports:
pan:1: assertion violated (n>2) (at depth 90)
Spin also generates a trail counterexample Stored in eg8.pml.trail
We can replay the counterexample with guided execution We can also highlight the trace in the state diagram using
SpinSpider
31/76
Closer Look at Output
1 2 3 4 5 6 7 8 9
10 11 12 13
14 15
16 17 18 19 20 21 22 23 24 25 26 27
28
pan:1: assertion violated (n>2) (at depth 88) pan: wrote eg8.pml.trail
(Spin Version 6.4.8 — 2 March 2018) Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim – (none specified) assertion violations +
acceptance cycles –
invalid end states +
State-vector 36 byte (size of a state), depth reached 92 (longest path), errors: 1
(not selected)
138429 87813 226242 0
states (total number of states), stored states , matched
transitions (= stored+matched)
atomic steps
hash conflicts: 4500 (resolved)
Stats on memory usage (in Megabytes):
8.449 equivalent memory usage for states (stored*(State-vector + overhead)) 5.565 actual memory usage for states (compression: 65.86%)
state-vector as stored = 14 byte + 28 byte overhead 128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
134.003 total actual memory usage (memory used)
32/76
Inspecting the Trail from the Command Line
We could use $spin -t eg8.pml
1
2
3
4
5
6
7
8 finished = 2
n=2
spin: eg8.pml:18, Error: assertion violated spin: text of failed assertion: assert((n>2))
spin: trail ends after 89 steps #processes: 3
TIMES = 10 n=2
9 89: 10 89: 11 89:
proc 2 (Finish:1) eg8.pml:19 (state 4)
12
3 processes created
But this just shows the offending state, not the entire trail
33/76
Inspecting the Trail
Perhaps more informative is to use jSpin
1 P:1
0 P:1
1 P:1
Process
1 P:1 1) n = (temp+1)
1) else
1) else
1) temp = n
Statement
P(1):temp 0
Statement
Pid, Process type, line number (??), statement, vars
Process
0P:11) temp=n 0 1
P(1):temp n
34/76
Program Correctness Model-Checking Introduction to Promela
Assertion Based Model Checking
Turnstile Example
MEP
End States
35/76
Critical Section
bool wantP = false, wantQ = false;
active proctype P() { do ::
printf(“Non critical section P\n”); wantP = true;
printf(“Critical section P\n”); wantP = false
od
}
active proctype Q() { do ::
printf(“Non critical section Q\n”); wantQ = true;
printf(“Critical section Q\n”); wantQ = false
od
}
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16 17 18 19
Is mutual exclusion guaranteed? Use assertion
Assertion requires knowing number of processes in their CSs
36/76
Critical Section
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
17
18
19
20
21
22 37/76
bool wantP = false, wantQ = false;
byte critical = 0;
active proctype P() { do ::
printf(“Non critical section P\n”); wantP = true;
critical ++;
assert (critical == 1); critical –;
printf(“Critical section P\n”);
wantP = false od
proctype Q() {
printf(“Non critical section Q\n”); wantQ = true;
}
active do ::
critical ++;
assert (critical == 1); critical –;
printf(“Critical section Q\n”);
Critical Section
Result of verification:
pan:1: assertion violated (critical<=1) (at depth 20)
Let’s check the trail generated by spin
Shorter counterexample produced by Random
Non critical section Q
1 Q:1 1) printf(’Non cr Non critical section P
0 P:1
1 Q:1
Process
0P:1
Process
1 Q:1
Process
0 P:1
spin: cs.pml:25, Error: assertion violated
1) printf(’Non cr
1) wantQ = 1
Statement wantQ
1) wantP=1 1
Statement wantP wantQ
1) critical = (cr 1 1
Statement critical wantP wantQ 1) critical = (cr 1 1 1
1 2 3 4 5 6 7 8 9
10 11 12
38/76
Revisiting Attempt III
global boolean wantP = false; global boolean wantQ = false;
1 2
1 2 3 4 5 6 7 8 9
10
Mutex: Yes
Absence deadlock: No (we’ll prove this using spin) Free from starvation: No
39/76
thread P: { 1 while (true) { 2 // non-critical section3 wantP = true; 4 await !wantQ; 5 // CRITICAL SECTION 6 wantP = false; 7 // non-critical section8 }9 } 10
thread Q: { while (true) {
// non-critical section
wantQ = true;
await !wantP;
// CRITICAL SECTION wantQ = false;
// non-critical section
} }
Attempt III in Promela
bool wantP = false, wantQ = false; byte critical = 0;
active proctype P() { do ::
printf("Non critical section P\n"); wantP = true;
wantQ == false;
critical ++;
assert (critical <= 1); critical --;
printf("Critical section P\n"); wantP = false
od
}
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15
We only list P, the full code is on the next slide
Recall that an expression is executable iff it returns true The expr on line 9 blocks until it is true
40/76
Attempt III – Abbreviated
bool wantP = false, wantQ = false; byte critical = 0;
active proctype P() { do ::
od
}
wantP = true;
!wantQ;
critical ++;
assert (critical <= 1); critical --;
wantP = false
1 2 3 4 5 6 7 8 9
10 11 12 13
41/76
Verifying Attempt III
Verification in spin reports pan:1: invalid end state (at depth 4)
What is an invalid state? All outgoing arrows point to same state
Here is the trail produced by spin
42/76
Attempt III – Fix
One easy fix is to have lines 5 and 6 below executed atomically The same for lines 13 and 14 below
bool wantP = false, wantQ = false;
active proctype P() { do ::
od
}
wantP = true; !wantQ;
wantP = false
active proctype Q() { do ::
}
od
wantQ = true; !wantP;
wantQ = false
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16 17
43/76
Attempt III - Fix
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
17
18
19
20
21
22 44/76
bool wantP = false, wantQ = false;
active do ::
proctype P() {
printf("Noncritical section P\n"); atomic {
!wantQ;
wantP = true }
printf("Critical section P\n"); wantP = false
proctype Q() {
printf("Noncritical section Q\n"); atomic {
!wantP;
wantQ = true }
printf("Critical section Q\n");
od
}
active do ::
Attempt III with Fix – Verification
Spin reports not errors: ••• errors: 0 •••
This means that there is not deadlock
Exercise: Add assertions to check for mutual exclusion Another possible fix
Back off if there is contention
This leads to our attempt IV (from the second set of slides of this course)
45/76
Revisiting Attempt IV
1 2
1 2 3 4 5 6 7 8 9
10 11 12 13
global boolean wantP = false; global boolean wantQ = false;
Mutex: Yes
Absence deadlock: Yes Free from starvation: No
46/76
thread P: { 1 while (true) { 2 // non-critical section3 wantP = true; 4 while wantQ { 5 wantP = false; 6 wantP = true; 7 }8 // CRITICAL SECTION 9 wantP = false; 10 // non-critical section11 } 12 } 13
thread Q: { while (true) {
// non-critical section wantQ = true;
while wantP {
wantQ = false;
wantQ = true; }
// CRITICAL SECTION wantQ = false;
// non-critical section
} }
Revisiting Attempt IV
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
17
18
19
20
21
22 47/76
bool wantP = false, wantQ = false;
active proctype P() { do
:: wantP = true; do
:: wantQ -> wantP = false; wantP = true :: else -> break
od;
wantP = false
od
}
active proctype Q() { do
:: wantQ = true; do
:: wantP -> wantQ = false; wantQ = true :: else -> break
od;
wantQ = false od
Revisiting Attempt IV
Check that there is no deadlock using spin Add assertions to check for mutual exclusion
48/76
Exercise: Write Dekker’s Algorithm in Promela
1 2 3
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16
global int turn = 1;
global boolean wantP = false; global boolean wantQ = false;
Right to insist on entering is passed between the two processes
49/76
thread P: { 1 while (true) { 2 // non-CS 3 wantP = true; 4 while wantQ 5 if(turn==2){ 6 wantP = false; 7 await (turn==1);8 wantP = true; 9 } 10 // CS 11 turn = 2; 12 wantP = false; 13 // non-CS 14 15 16
}
}
thread Q: { while (true) {
// non-CS
wantQ = true; while wantP
if (turn == 1) { wantQ = false; await (turn==2); wantQ = true;
}
// CS
turn = 1; wantQ = false; // non-CS
} }
Exercise: Write Dekker’s Algorithm in Promela
1 2 3 4 5 6 7 8 9
10 11 12 13 14 15 16 17 18 19 20 21
bool wantp = false, wantq = false; byte turn = 1;
active proctype P() { do
:: wantp = true; do
:: !wantq -> break; :: else ->
if
:: (turn == 1) /* no statements, leaves if */ :: (turn == 2) ->
fi od;
wantp =
turn=2
od
}
wantp (turn wantp
false;
= false; == 1);
= true
50/76
Program Correctness Model-Checking Introduction to Promela
Assertion Based Model Checking
Turnstile Example MEP
End States
51/76
Additional Comment on End States
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
17
18
19
20
21
22 52/76
byte request = 0;
active proctype Server1() { do
:: request == 1 -> printf(“Service 1\n”);
request = 0;
od
}
active proctype Server2() {
do
:: request == 2 -> printf(“Service 2\n”);
request = 0;
od
}
active proctype Client() {
request = 1; request == 0; request = 2; request == 0;
}
Additional Comments on End States
A process that does not terminate in its last instruction is said to be in an invalid end state
Servers are always blocked at the guard of the do-statement waiting for it to become executable
To avoid this: use a label to indicate that a control point is a valid end point, even if it is not the last instruction
active proctype Server1() { endserver:
do
:: request == 1 -> …
od
}
1 2 3 4 5 6
53/76
Appendix
Installing Spin and jSpin
More Details on Promela Syntax
54/76
Installing Spin
Binaries: https://github.com/nimble-code/Spin
Uncompress and make executable (chmod +x spin645 mac)
55/76
Installing jSpin
Installing jSpin
Download:
http://www.weizmann.ac.il/sci-tea/benari/
software-and-learning-materials/jspin
Compile and create .jar file
Configuration:
Create a jspin-5-0/bin directory
Add binary file for spin in jspin-5-0/bin (eg. spin645 mac). Modify the following items in config.cfg:
SPIN=../bin/spin645_mac
C_COMPILER=/usr/bin/gcc
DOT=/usr/local/bin/dot
Somewhat outdated reference manual: http: //wwinf.u-szeged.hu/~gombas/HSRV/jspin-user.pdf
56/76
Emacs and Dot
Emacs
Promela mode:
https://github.com/rudi/promela-mode
Place in ~ /.emacs.d/plugins Install by adding this to .emacs
(add-to-list ’load-path “~/.emacs.d/plugins”) (require ’promela-mode)
Install dot
brew install graphviz
57/76
Execution using Spin/jSpin
From command line: ../bin/spin645 mac count.pml
Using jSpin
Modes:
Random
Interactive
Guided: follows the error trail that was produced by an earlier
verification (not presented yet) run
58/76
Bibliography
Principles of the Spin Model Checker, Mordechai Ben-Ari, Springer, 2008 (reprinted April 11, 2013).
http://spinroot.com/spin/Doc/SpinTutorial.pdf
59/76
Appendix
Installing Spin and jSpin
More Details on Promela Syntax
60/76
Promela Summary
FEATURE
C
PROMELA
integers
char, short, int, long
byte, short, int
bit field
unsigned
unsigned
floats
float, double
NONE
boolean
int
bool
strings
char, char*
NONE
arrays
yes
1D & limited
operators
many
mostly same
if
as usual
similar to Erlang
loops
while, for, do
do, similar to if
output
printf
printf
input
scanf
NONE
functions
yes
NO
pointers
yes
NO
enum
enum
mtype
comments
/* */ and //
/* */
cpp
full
1-line #define, #include
61/76
If Syntax
“Guarded commands” wrapped inside “if … fi”
disc = b*b – 4*a*c;
if
:: disc > 0 ->
printf(“two real roots\n”)
:: disc < 0 ->
printf(“no real roots\n”)
:: disc == 0 ->
printf(“duplicate real roots\n”)
fi
1 2 3 4 5 6 7 8 9
62/76
If Semantics
First: evaluate all guards Then:
If no guard true: statement blocks until at least one guard becomes true (which could happen due to action of some concurrent process)
If one guard true: execute its command(s)
If more than one guard true: execute command(s) of randomly
chosen guard
63/76
Else
Guard consisting of “else” keyword is true if all other guards are blocked
Example:
1 2 3 4 5 6 7 8 9
disc = b*b – 4*a*c;
if
:: else ->
printf(“two real roots\n”)
:: disc < 0 ->
printf(“no real roots\n”)
:: disc == 0 ->
printf(“duplicate real roots\n”) fi
64/76
Do Syntax
Similar to if statement
Example: compute GCD by repeated subtraction
1 2 3 4 5 6 7
Notes:
• No loop test; only way out is via break • Body consists of guarded commands
• Some true guard is chosen at random
• Block if no true guard
/* assume x and y are initialized */
int a = x, b = y;
do :: a > b -> a = a – b
:: b > a -> b = b – a
:: a == b -> break od
printf(“GCD(%d, %d) = %d\n”, x, y, a);
65/76
Do Semantics
Promela has no other type of loop
Most common loop has only 2 guarded commands:
1 2 3 4
This structure provides deterministic operation like:
1 2
do
:: [exit test] -> break
:: else -> [body statements]
od
while (not [exit test])
{ [body statements] }
66/76
Another Example
proctype P() {
int x = 15, y = 20; int a = x, b = y;
do
:: a > b ->
:: b > a ->
:: a == b ->
od
printf(“GCD(%d, %d) = %d\n”, x, y, a);
}
a = a – b b = b – a break
1 2 3 4 5 6 7 8 9
10 11
Note:
proctype P() declares no-argument program P Can include arguments:
1 2 3
proctype P(int x, int y) { int a = x, b = y;
etc. }
67/76
Spawning a Process
Can start processes using run operator: run P(15, 20) Also, can declare process with active proctype
Adding “active” means “define and run this program” To start two processes executing same code, use:
active [2] proctype P(int x, int y)
Can create an initial process that runs before any of the “proctype” processes
This process must be named init
68/76
Predefined Variables
_pid is process ID
_nr_pr is number of active processes Examples:
1 printf(“process %d: n goes from %d to %d\n”, _pid, temp, n); 2
3 if
4 :: _nr_pr == 1 -> printf(“at end n = %d\n”, n);
5 fi
69/76
Blocking Statements, I
Concurrent programs must often wait for some event Possible to guard any statement
This:
_nr_pr == 1 -> printf(“at end n = %d\n”, n)
is the same as:
1 2 3
1
if
:: _nr_pr == 1 -> printf(“at end n = %d\n”, n) fi
70/76
Blocking Statements, II
“->” arrow is just syntactic sugar
Can write expression by itself; if it doesn’t evaluate to
non-zero then program will block This:
_nr_pr == 1;
printf(“at end n = %d\n”, n)
1 2
1
is the same as:
_nr_pr == 1 -> printf(“at end n = %d\n”, n)
71/76
Atomicity, I
Individual Promela statements are atomic
Warning! In Promela, expressions are statements too (hence expressions are atomic)
Example – here, division by zero is possible:
1 2 3 4
In an if (and do) statement, interleaving may occur between the evaluation of the guard and the execution of the statement after the guard
if
:: else -> c = b fi
:: a != 0 -> c = b / a ;
72/76
Atomicity, II
It is tempting to regard the entirety of a != 0 -> c = b / a as atomic
Butitconsistsoftwoatomicparts,a != 0 andc = b / a
Remember that this:
1 a != 0 -> c = b / a
could be written as:
1 2
The latter more obviously contains two atomic parts
a != 0; /* may block */ c=b/a
73/76
Atomicity, III
To group statements together atomically use atomic
atomic {
a != 0; /* may block */ c=b/a
}
1 2 3 4
If any statement within the atomic sequence blocks, atomicity is lost, and other processes may start executing statements.
When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time (but it has to compete with other active processes)
74/76
Atomic & Run
run only starts a concurrent process
atomic prevents execution of any other actions besides those in
its body
Therefore, to start a group of processes that should run concurrently:
atomic {
run P1 (…);
run P2 (…); …
run PN (…) }
1 2 3 4 5 6
At conclusion of atomic block: all processes have been started but none is yet running
75/76
Variable Size
Use smallest integer variable that will fit the need
E.g., for integers known to be small use “byte” (8 bits)
instead of “int” (32 bits)
Reason: “verification” simulates all possible values of variable
76/76