Proof Score for the Mutual Exclusion Property of
QLOCK
(You can download .zip file of this whole directory from
here.)
The following sequence of files shows an example process of developing
specification and proof score for the mutual exclusion property
of Qlock protocol. It is recommended for readers to check
that proof-N.cafe can be
obtained
by applying legitimate splittings and/or transformations to some of
proof passage(s) in proof-(N-1).cafe
for 00 < N < 22. Notice
that proof-N.cafe (N = 00
... 05) is making use of only invariants-0.cafe
and proof-N.cafe (N = 06
... 09) is making use of only invariants-1.cafe,
and proof-N.cafe (N = 10
... 21) is making use of invariants-2.cafe
.
- qlock.cafe The
specification of the Qlock protocol as the module QLOCK
- invariants-0.cafe
0th invariant file defining INV1 making use of QLOCK
- invariants-1.cafe
1st invariant file defining ISTEP1 making use of INV1
- invariants-2.cafe
the final invariant file defining INV2 and ISTEP2 making use of ISTEP1
and INV2 respectively.
- proof-00.cafe 00th
proof
score file making use of INV1
- proof-01.cafe 01th
proof
score file making use of INV1
- proof-02.cafe 02th
proof
score file making use of INV1
- proof-03.cafe 03th
proof
score file making use of INV1
- proof-04.cafe 04th
proof
score file making use of INV1
- proof-05.cafe 05th
proof
score file making use of INV1
- proof-06.cafe 06th
proof
score file making use of INV1+ISTEP1
- proof-07.cafe 07th
proof
score file making use of INV1+ISTEP1
- proof-08.cafe 08th
proof
score file making use of INV1+ISTEP1
- proof-09.cafe 09th
proof
score file making use of INV1+ISTEP1
- proof-10.cafe 10th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-11.cafe 11th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-12.cafe 12th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-13.cafe 13th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-14.cafe 14th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-15.cafe 15th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-16.cafe 16th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-17.cafe 17th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-18.cafe 18th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-19.cafe 19th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-20.cafe 20th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-21.cafe the
final
proof score file making use of INV1+ISTEP1+INV2+ISTEP2.
Notice that you do not need to prepare all of the above files.
Only the files qlock.cafe,
invariants-2.cafe, and proof-21.cafe
consititute a complete suite of specification and effective proof scroe
for the
mutual exclusion property of the Qlock protocol.
- simultaneous induction
scheme which is used to construct assertions/proof-passages in the
file proof-10.cafe from the ones in the file proof-09.cafe