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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
(**
{1 VerifyThis @ ETAPS 2018 competition
Challenge 3: Array-Based Queuing Lock}
Author: Martin Clochard (LRI, Université Paris Sud)
*)
use int.Int
use int.ComputerDivision
use import seq.Seq as S
use array.Array
use ref.Ref
val constant k : int ensures { result > 0 }
val constant n : int ensures { result > 0 }
(* Model of bounded arithmetic.
Note: bincrement only model the incrementation behind fetch_and_add,
not the atomic operation itself. *)
type bounded_int = private { ghost bmodel : int }
invariant { 0 <= bmodel < k * n } by { bmodel = 0 }
val constant bzero : bounded_int
ensures { result.bmodel = 0 }
val bincrement (b:bounded_int) : bounded_int
ensures { let v = b.bmodel + 1 in
result.bmodel = if v = k * n then 0 else v }
val bmodn (b:bounded_int) : int
ensures { result = mod b.bmodel n }
(* Minor ghost wrapping of the model to get rid of k from the model,
while keeping the same operational meaning. *)
type bounded_int2 = {
value : bounded_int;
ghost model : int;
} invariant { 0 <= model < n }
invariant { model = mod value.bmodel n }
by { value = bzero; model = 0 }
type ticket = { tvalue : int } invariant { 0 <= tvalue < n }
let zero () : bounded_int2
ensures { result.model = 0 }
= { value = bzero; model = 0 }
let increment (b:bounded_int2) : bounded_int2
ensures { let v = b.model + 1 in
result.model = if v = n then 0 else v }
= let ghost v0 = b.model in
let ghost v1 = if v0+1 = n then 0 else v0 + 1 in
let ghost v2 = b.value.bmodel in
assert { mod (v2+1) n = v1 by exists q.
v2 = n * q + v0 so q >= 0 so v2 + 1 = n * q + (v0+1)
so if v0+1 < n then v0+1 = mod (v2+1) n else
v2+1 = n * (q+1) + 0 so 0 = mod (v2+1) n };
{ value = bincrement b.value; model = v1 }
let modn (b:bounded_int2) : ticket
ensures { result.tvalue = b.model }
= { tvalue = bmodn b.value }
let tinc (t:ticket) : ticket
ensures { let v = t.tvalue + 1 in result.tvalue = if v = n then 0 else v }
= { tvalue = mod (t.tvalue + 1) n }
(* Break down the thread state between each operation that affect or
read the global state *)
type thread_state =
| AcqFetched ticket (* Corresponds to control point right after the fetch. *)
| Granted ticket (* Corresponds to observation that pass was true.
If it was false, there may be intermediate steps, but they do not
rely on global state --> state equivalent to lock granted. *)
| RelSet ticket (* Corresponds to the pass = false operation. *)
| Released ticket (* Corresponds to a released state.
for technical reasons, we keep the last ticket used here
(which is defaulted to the thread id at the beginning *)
function ticket (s:thread_state) : int = match s with
| AcqFetched t | Granted t | RelSet t | Released t -> t.tvalue
end
predicate released (s:thread_state) = match s with
| Released _ -> true | _ -> false
end
(* For verification of task 2: log of request/acquire events
identified by thread id. *)
type event =
| Request int
| Acquire int
type hidden = private mutable {}
val hidden : hidden
(* scheduler. *)
val schedule () : int
writes { hidden }
ensures { 0 <= result < n }
(* if a thread is in a granted or released state,
check whether it begins an acquire or release. Otherwise,
the state stays the same. *)
val acqrel (id: int) : bool
writes { hidden }
(* Model execution of concurrent program. *)
let main () : unit
diverges
= (* Model of the pass buffer. The begin-end block with post-condition
hide the fact that the array was technically initialized. *)
let pass = begin ensures { result.length = n } make n false end in
(* Model of the next variable. *)
let next = ref (zero ()) in
(* Thread state. *)
let state = make n (Released { tvalue = 0 }) in
(* Additional reciprocal map for the cyclically allocated tickets. *)
let tmap = make n 0 in
for i = 0 to n - 1 do
invariant { forall j. 0 <= j < i -> match state[j] with
| Released t -> t.tvalue = j
| _ -> false end }
invariant { forall j. 0 <= j < i -> tmap[j] = j }
state[i] <- Released { tvalue = i };
tmap[i] <- i
done;
(* Extra variable for verification: index of the currently held ticket. *)
let current = ref (modn (zero ())) in
(* Event log (for second task). *)
(* let log = ref empty in *)
(* Initialisation, done before the threads are executed. *)
for i = 1 to n - 1 do
invariant { forall j. 1 <= j < i -> not pass[j] }
pass[i] <- false;
done;
pass[0] <- true;
while true do
invariant { forall i. 0 <= i < n /\ pass[i] -> i = !current.tvalue }
invariant { forall i. 0 <= i < n -> match state[i] with
| Granted t -> t.tvalue = !current.tvalue /\ pass[t.tvalue]
| RelSet t -> t.tvalue = !current.tvalue /\ not pass[t.tvalue]
| _ -> true
end
}
invariant { forall i. 0 <= i < n -> 0 <= tmap[i] < n }
invariant { forall i. 0 <= i < n -> ticket state[tmap[i]] = i }
invariant { forall i. 0 <= i < n -> tmap[ticket state[i]] = i }
invariant { !next.model < !current.tvalue ->
(forall i. 0 <= i < !next.model \/ !current.tvalue <= i < n ->
not released state[tmap[i]])
/\ (forall i. !next.model <= i < !current.tvalue ->
released state[tmap[i]]) }
invariant { !next.model > !current.tvalue ->
(forall i. !current.tvalue <= i < !next.model ->
not released state[tmap[i]])
/\ (forall i. 0 <= i < !current.tvalue \/ !next.model <= i < n ->
released state[tmap[i]]) }
invariant { !next.model = !current.tvalue ->
forall i j. 0 <= i < j < n ->
released state[tmap[i]] <-> released state[tmap[j]] }
(* Invariant corresponding to Task 1, slightly strengthened. *)
invariant { forall i j. 0 <= i < j < n ->
match state[i], state[j] with
| (Granted _ | RelSet _), (Granted _ | RelSet _) -> false
| _ -> true end
}
let id = schedule () in
match state[id] with
| AcqFetched ticket ->
if pass[ticket.tvalue] then state[id] <- Granted ticket
| Granted ticket -> if acqrel id then begin
state[id] <- RelSet ticket;
pass[ticket.tvalue] <- false;
end
| RelSet ticket ->
state[id] <- Released ticket;
pass[(tinc ticket).tvalue] <- true;
current := tinc !current;
| Released told -> if acqrel id then begin
let ticket = modn !next in
let id2 = tmap[ticket.tvalue] in
match state[id2] with
| Released _ -> state[id2] <- Released told;
tmap[ticket.tvalue] <- id;
tmap[told.tvalue] <- id2
| _ -> absurd
end;
state[id] <- AcqFetched ticket;
next := increment !next
end
end
done
|
