:: Event-based Proof of the Mutual Exclusion Property of {P}eterson's Algorithm
:: by Ievgen Ivanov , Mykola Nikitchenko and Uri Abraham
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

:: --------------------- Preliminaries ------------------------

definition

attr c₁ is strict ;
struct Values_with_TF -> 1-sorted ;
aggr Values_with_TF(# carrier, True, False #) -> Values_with_TF ;
sel True c₁ -> Element of the carrier of c₁;
sel False c₁ -> Element of the carrier of c₁;

end;

definition

let A be Values_with_TF ;

attr A is consistent means :: PETERSON:def 1
the True of A <> the False of A;

end;

:: deftheorem defines consistent PETERSON:def 1 :
for A being Values_with_TF holds
( A is consistent iff the True of A <> the False of A );

registration

cluster consistent for Values_with_TF ;

existence
ex b₁ being Values_with_TF st b₁ is consistent

proof end;

end;

definition

mode Values_with_Bool is consistent Values_with_TF ;

end;

definition

let A be RelStr ;

attr A is strongly_connected means :: PETERSON:def 2
the InternalRel of A is_strongly_connected_in the carrier of A;

end;

:: deftheorem defines strongly_connected PETERSON:def 2 :
for A being RelStr holds
( A is strongly_connected iff the InternalRel of A is_strongly_connected_in the carrier of A );

registration

cluster non empty reflexive transitive strongly_connected for RelStr ;

existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ is reflexive & b₁ is transitive & b₁ is strongly_connected )

proof end;

end;

definition

mode LinearPreorder is reflexive transitive strongly_connected RelStr ;

end;

:: ---------------------- Main structure -----------------------

definition

let Values be Values_with_Bool;
attr c₂ is strict ;
struct Events_structure over Values -> ;
aggr Events_structure(# events, processes, locations, traces, procE, traceE, readE, writeE, val_of #) -> Events_structure over Values;
sel events c₂ -> non empty LinearPreorder;
sel processes c₂ -> non empty set ;
sel locations c₂ -> non empty set ;
sel traces c₂ -> non empty set ;
sel procE c₂ -> Function of the processes of c₂,(bool the carrier of the events of c₂);
sel traceE c₂ -> Function of the traces of c₂,(bool the carrier of the events of c₂);
sel readE c₂ -> Function of the locations of c₂,(bool the carrier of the events of c₂);
sel writeE c₂ -> Function of the locations of c₂,(bool the carrier of the events of c₂);
sel val_of c₂ -> PartFunc of the carrier of the events of c₂, the carrier of Values;

end;

:: ---------------------- Modes ---------------------------

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
mode Process of S is Element of the processes of S;
mode Event of S is Element of the carrier of the events of S;
mode EventSet of S is Subset of the carrier of the events of S;
mode Location of S is Element of the locations of S;
mode trace of S is Element of the traces of S;

end;

:: ----------------Predicates, functors, notation ---------------

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;
let x be Location of S;

pred e reads x means :: PETERSON:def 3
e in the readE of S . x;

pred e writesto x means :: PETERSON:def 4
e in the writeE of S . x;

end;

:: deftheorem defines reads PETERSON:def 3 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S holds
( e reads x iff e in the readE of S . x );

:: deftheorem defines writesto PETERSON:def 4 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S holds
( e writesto x iff e in the writeE of S . x );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let x be Location of S;
let E be EventSet of S;

pred E reads x means :: PETERSON:def 5
ex e being Event of S st
( e in E & e reads x );

pred E writesto x means :: PETERSON:def 6
ex e being Event of S st
( e in E & e writesto x );

end;

:: deftheorem defines reads PETERSON:def 5 :
for Values being Values_with_Bool
for S being Events_structure over Values
for x being Location of S
for E being EventSet of S holds
( E reads x iff ex e being Event of S st
( e in E & e reads x ) );

:: deftheorem defines writesto PETERSON:def 6 :
for Values being Values_with_Bool
for S being Events_structure over Values
for x being Location of S
for E being EventSet of S holds
( E writesto x iff ex e being Event of S st
( e in E & e writesto x ) );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;
let tr be trace of S;

pred e in tr means :: PETERSON:def 7
e in the traceE of S . tr;

end;

:: deftheorem defines in PETERSON:def 7 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for tr being trace of S holds
( e in tr iff e in the traceE of S . tr );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;
let p be Process of S;

pred e in p means :: PETERSON:def 8
e in the procE of S . p;

end;

:: deftheorem defines in PETERSON:def 8 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for p being Process of S holds
( e in p iff e in the procE of S . p );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;

func val e -> object equals :: PETERSON:def 9
the val_of of S . e;

correctness
coherence
the val_of of S . e is object ;
;

end;

:: deftheorem defines val PETERSON:def 9 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S holds val e = the val_of of S . e;

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;
let p be Process of S;
let tr be trace of S;

pred e in p,tr means :: PETERSON:def 10
( e in p & e in tr );

end;

:: deftheorem defines in PETERSON:def 10 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for p being Process of S
for tr being trace of S holds
( e in p,tr iff ( e in p & e in tr ) );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;
let e be Event of S;
let x be Location of S;
let a be Element of the carrier of Values;

pred e writesto x,a means :: PETERSON:def 11
( e writesto x & val e = a );

pred e reads x,a means :: PETERSON:def 12
( e reads x & val e = a );

end;

:: deftheorem defines writesto PETERSON:def 11 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S
for a being Element of the carrier of Values holds
( e writesto x,a iff ( e writesto x & val e = a ) );

:: deftheorem defines reads PETERSON:def 12 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S
for a being Element of the carrier of Values holds
( e reads x,a iff ( e reads x & val e = a ) );

::------------------ Attributes -----------------------

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;

attr S is pr-complete means :: PETERSON:def 13
for tr being trace of S
for e being Event of S st e in tr holds
ex p being Process of S st e in p;

attr S is pr-ordered means :: PETERSON:def 14
for p being Process of S
for e1, e2 being Event of S st e1 in p & e2 in p & e1 <= e2 & e2 <= e1 holds
e1 = e2;

attr S is rw-ordered means :: PETERSON:def 15
for x being Location of S
for e1, e2 being Event of S st ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 holds
e1 = e2;

attr S is rw-consistent means :: PETERSON:def 16
for tr being trace of S
for x being Location of S
for e being Event of S
for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds
ex e0 being Event of S st
( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of S st e1 in tr & e1 <= e & e1 writesto x holds
e1 <= e0 ) );

attr S is rw-exclusive means :: PETERSON:def 17
for e being Event of S
for x1, x2 being Location of S holds
( not e reads x1 or not e writesto x2 );

end;

:: deftheorem defines pr-complete PETERSON:def 13 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is pr-complete iff for tr being trace of S
for e being Event of S st e in tr holds
ex p being Process of S st e in p );

:: deftheorem defines pr-ordered PETERSON:def 14 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is pr-ordered iff for p being Process of S
for e1, e2 being Event of S st e1 in p & e2 in p & e1 <= e2 & e2 <= e1 holds
e1 = e2 );

:: deftheorem defines rw-ordered PETERSON:def 15 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-ordered iff for x being Location of S
for e1, e2 being Event of S st ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 holds
e1 = e2 );

:: deftheorem defines rw-consistent PETERSON:def 16 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-consistent iff for tr being trace of S
for x being Location of S
for e being Event of S
for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds
ex e0 being Event of S st
( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of S st e1 in tr & e1 <= e & e1 writesto x holds
e1 <= e0 ) ) );

:: deftheorem defines rw-exclusive PETERSON:def 17 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-exclusive iff for e being Event of S
for x1, x2 being Location of S holds
( not e reads x1 or not e writesto x2 ) );

definition

let Values be Values_with_Bool;
let S be Events_structure over Values;

attr S is consistent means :: PETERSON:def 18
( S is pr-complete & S is pr-ordered & S is rw-ordered & S is rw-consistent & S is rw-exclusive );

end;

:: deftheorem defines consistent PETERSON:def 18 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is consistent iff ( S is pr-complete & S is pr-ordered & S is rw-ordered & S is rw-consistent & S is rw-exclusive ) );

registration

let Values be Values_with_Bool;

cluster consistent for Events_structure over Values;

existence
ex b₁ being Events_structure over Values st b₁ is consistent

proof end;

end;

definition

let Values be Values_with_Bool;
mode DistributedSysWithSharedMem of Values is consistent Events_structure over Values;

end;

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let e1, e2 be Event of DS;

pred e1 << e2 means :: PETERSON:def 19
( e1 <= e2 & not e2 <= e1 );

end;

:: deftheorem defines << PETERSON:def 19 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( e1 << e2 iff ( e1 <= e2 & not e2 <= e1 ) );

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let e1, e2 be Event of DS;

func (e1,e2) inter -> EventSet of DS equals :: PETERSON:def 20
{ e where e is Event of DS : ( e1 < e & e < e2 ) } ;

correctness
coherence
{ e where e is Event of DS : ( e1 < e & e < e2 ) } is EventSet of DS;

proof end;

end;

:: deftheorem defines inter PETERSON:def 20 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds (e1,e2) inter = { e where e is Event of DS : ( e1 < e & e < e2 ) } ;

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let e1, e2 be Event of DS;
let p be Process of DS;
let tr be trace of DS;

func (e1,e2) interval_in (p,tr) -> EventSet of DS equals :: PETERSON:def 21
{ e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } ;

correctness
coherence
{ e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } is EventSet of DS;

proof end;

end;

:: deftheorem defines interval_in PETERSON:def 21 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS
for p being Process of DS
for tr being trace of DS holds (e1,e2) interval_in (p,tr) = { e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } ;

theorem :: PETERSON:1

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

proof end;

theorem thLinPreordEvents: :: PETERSON:2

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( e1 <= e2 or e2 <= e1 )

proof end;

theorem :: PETERSON:3

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e, e1, e2 being Event of DS st e in p,tr & e1 < e & e < e2 holds
e in (e1,e2) interval_in (p,tr) ;

theorem :: PETERSON:4

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS st e1 < e2 holds
e1 <= e2 by ORDERS_2:def 6;

theorem thEvStrictPrec: :: PETERSON:5

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for e1, e2 being Event of DS st e1 in p & e2 in p & e1 < e2 holds
e1 << e2

proof end;

theorem :: PETERSON:6

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e1, e2 being Event of DS st e1 in p,tr & e2 in p,tr & e1 < e2 holds
e1 << e2 by thEvStrictPrec;

theorem :: PETERSON:7

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS st e1 << e2 holds
e1 < e2 by ORDERS_2:def 6;

theorem :: PETERSON:8

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for e1, e2 being Event of DS st e1 in p & e2 in p & not e1 = e2 & not e1 << e2 holds
e2 << e1 by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;

theorem thEvTrans: :: PETERSON:9

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 <= e2 & e2 <= e3 holds
e1 <= e3

proof end;

theorem thEvStrictTrans1: :: PETERSON:10

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 <= e2 & e2 << e3 holds
e1 << e3 by thEvTrans;

theorem thEvStrictTrans2: :: PETERSON:11

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 << e2 & e2 <= e3 holds
e1 << e3 by thEvTrans;

theorem :: PETERSON:12

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 << e2 & e2 << e3 holds
e1 << e3 by thEvTrans;

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let e1, e2 be Event of DS;

:: simultaneous events

pred simultev e1,e2 means :: PETERSON:def 22
( e1 <= e2 & e2 <= e1 );

end;

:: deftheorem defines simultev PETERSON:def 22 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( simultev e1,e2 iff ( e1 <= e2 & e2 <= e1 ) );

theorem :: PETERSON:13

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( simultev e1,e2 or e1 << e2 or e2 << e1 ) by thLinPreordEvents;

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let p be Process of DS;
let tr be trace of DS;
let e be Event of DS;
let x1, x2, turn be Location of DS;
let a1, a2 be Element of the carrier of Values;

pred e has_Peterson_mutex_in p,x1,x2,turn,a1,a2,tr means :: PETERSON:def 23
ex e1, e2, e3 being Event of DS st
( e1 in p,tr & e2 in p,tr & e3 in p,tr & e1 < e2 & e2 < e3 & e3 < e & e1 writesto x1, the True of Values & not (e1,e) interval_in (p,tr) writesto x1 & e2 writesto turn,a2 & not (e2,e) interval_in (p,tr) writesto turn & ( e3 reads x2, the False of Values or e3 reads turn,a1 ) );

end;

:: deftheorem defines has_Peterson_mutex_in PETERSON:def 23 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e being Event of DS
for x1, x2, turn being Location of DS
for a1, a2 being Element of the carrier of Values holds
( e has_Peterson_mutex_in p,x1,x2,turn,a1,a2,tr iff ex e1, e2, e3 being Event of DS st
( e1 in p,tr & e2 in p,tr & e3 in p,tr & e1 < e2 & e2 < e3 & e3 < e & e1 writesto x1, the True of Values & not (e1,e) interval_in (p,tr) writesto x1 & e2 writesto turn,a2 & not (e2,e) interval_in (p,tr) writesto turn & ( e3 reads x2, the False of Values or e3 reads turn,a1 ) ) );

definition

let Values be Values_with_Bool;
let DS be DistributedSysWithSharedMem of Values;
let tr be trace of DS;
let Es be set ;

pred Es has_Peterson_mutex_in tr means :: PETERSON:def 24
ex p1, p2 being Process of DS st
( ( for p being Process of DS holds
( p = p1 or p = p2 ) ) & ex flag1, flag2, turn being Location of DS st
( ( for e being Event of DS st e in p1,tr holds
( not e writesto flag2 & not e writesto turn, the False of Values ) ) & ( for e being Event of DS st e in p2,tr holds
( not e writesto flag1 & not e writesto turn, the True of Values ) ) & ( for e being Event of DS st e in Es holds
( e has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr ) ) ) );

end;

:: deftheorem defines has_Peterson_mutex_in PETERSON:def 24 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for tr being trace of DS
for Es being set holds
( Es has_Peterson_mutex_in tr iff ex p1, p2 being Process of DS st
( ( for p being Process of DS holds
( p = p1 or p = p2 ) ) & ex flag1, flag2, turn being Location of DS st
( ( for e being Event of DS st e in p1,tr holds
( not e writesto flag2 & not e writesto turn, the False of Values ) ) & ( for e being Event of DS st e in p2,tr holds
( not e writesto flag1 & not e writesto turn, the True of Values ) ) & ( for e being Event of DS st e in Es holds
( e has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr ) ) ) ) );

theorem lemwbefr: :: PETERSON:14

for Values being Values_with_Bool
for a1, a2 being Element of the carrier of Values
for DS being DistributedSysWithSharedMem of Values
for x being Location of DS
for tr being trace of DS
for e1, e2 being Event of DS st e1 in tr & e2 in tr & e1 reads x,a1 & e2 reads x,a2 & e1 <= e2 & a1 <> a2 holds
ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 )

proof end;

:: Main result: Mutual exclusion property of Peterson's algorithm

theorem :: PETERSON:15

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for tr being trace of DS
for e1, e2 being Event of DS st e1 in tr & e2 in tr & {e1,e2} has_Peterson_mutex_in tr & not e1 = e2 & not e1 << e2 holds
e2 << e1

proof end;