:: 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-2025 Association of Mizar Users


:: --------------------- Preliminaries ------------------------
definition
attr c1 is strict ;
struct Values_with_TF -> 1-sorted ;
aggr Values_with_TF(# carrier, True, False #) -> Values_with_TF ;
sel True c1 -> Element of the carrier of c1;
sel False c1 -> Element of the carrier of c1;
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 b1 being Values_with_TF st b1 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 b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 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 c2 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 c2 -> non empty LinearPreorder;
sel processes c2 -> non empty set ;
sel locations c2 -> non empty set ;
sel traces c2 -> non empty set ;
sel procE c2 -> Function of the processes of c2,(bool the carrier of the events of c2);
sel traceE c2 -> Function of the traces of c2,(bool the carrier of the events of c2);
sel readE c2 -> Function of the locations of c2,(bool the carrier of the events of c2);
sel writeE c2 -> Function of the locations of c2,(bool the carrier of the events of c2);
sel val_of c2 -> PartFunc of the carrier of the events of c2, 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 b1 being Events_structure over Values st b1 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;

:: WP: 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;