-
Notifications
You must be signed in to change notification settings - Fork 2
/
mypyvy.pyv
82 lines (70 loc) · 2.75 KB
/
mypyvy.pyv
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
# This is a specification of a simple concurrent algorithm from the paper
# "Teaching Concurrency" by Leslie Lamport. In there are N processes and
# two arrays of length N, x and y. Each process i executes the following
# sequence of statements:
# x[i] := 1;
# y[i] := x[(i-1) mod N];
# The reads and writes of each x[j] are assumed to be atomic. This
# algorithm has the property that once all processes have finished, at
# least one y[j] == 1.
#
# It doesn't really matter which q a process p reads x[q] from (even q=p
# works). Informally, any choice of q works because when the last process
# writes y, all elements of x have been set to one. So the specification
# below generalizes the algorithm from the paper. I really did this
# because it would have been a pain to define ((i-1) mod N) in mypyvy.
# PC labels
sort label
# processes that write to x and y
sort process
# values the elements of x and y arrays can take
sort value
# Each process executes two atomic steps in sequence, an update to x, then
# an update to y. This requires three labels, the initial one (x_label),
# after updating x (y_label), and when the process has finished (done).
# These labels must be distinct.
immutable constant x_label: label
immutable constant y_label: label
immutable constant done: label
axiom x_label != y_label
axiom y_label != done
axiom done != x_label
# The set of possible values doesn't matter, except that there must exist
# at least one such value that processes can write to their element in the
# x array.
immutable constant one: value
# There are three arrays, x, y, and pc. The pc array tracks the label
# (control state) of each process.
mutable function x(process): value
mutable function y(process): value
mutable function pc(process): label
# All processes start at the x_label. The initial values of x and y don't
# matter.
init forall p. pc(p) = x_label
# First step:
# x[p] := 1
transition write_x(p: process)
modifies pc, x
& old(pc(p) = x_label)
& x(p) = one & (forall P. P != p -> x(P) = old(x(P)))
& pc(p) = y_label & (forall P. P != p -> pc(P) = old(pc(P)))
# Second step:
# y[p] := x[q] for some q
transition write_y(p: process, q: process)
modifies pc, y
& old(pc(p) = y_label)
& y(p) = old(x(q)) & (forall P. P != p -> y(P) = old(y(P)))
& pc(p) = done & (forall P. P != p -> pc(P) = old(pc(P)))
# The safety property: when all processes finish, there's some process
# that has set it's y element to one.
safety [safety_inv]
(forall P. pc(P) = done) ->
exists P. y(P) = one
# Conjoining the following to inv forms an inductive invariant. x_inv
# just records that a x[p] = 1 once a process has moved past x_label.
invariant [x_inv]
forall P. (pc(P) = y_label || pc(P) = done) -> x(P) = one
sat trace { # sanity check
write_x
write_y
}