:: by Ievgen Ivanov , Mykola Nikitchenko and Uri Abraham

::

:: Received August 14, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

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

definition

attr c_{1} is strict ;

struct Values_with_TF -> 1-sorted ;

aggr Values_with_TF(# carrier, True, False #) -> Values_with_TF ;

sel True c_{1} -> Element of the carrier of c_{1};

sel False c_{1} -> Element of the carrier of c_{1};

end;
struct Values_with_TF -> 1-sorted ;

aggr Values_with_TF(# carrier, True, False #) -> Values_with_TF ;

sel True c

sel False c

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

for A being Values_with_TF holds

( A is consistent iff the True of A <> the False of A );

definition

let A be RelStr ;

end;
attr A is strongly_connected means :: PETERSON:def 2

the InternalRel of A is_strongly_connected_in the carrier of A;

the InternalRel of A is_strongly_connected_in the carrier of A;

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

for A being RelStr holds

( A is strongly_connected iff the InternalRel of A is_strongly_connected_in the carrier of A );

registration

existence

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is reflexive & b_{1} is transitive & b_{1} is strongly_connected )

end;
ex b

( not b

proof end;

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

definition

let Values be Values_with_Bool;

attr c_{2} 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_{2} -> non empty LinearPreorder;

sel processes c_{2} -> non empty set ;

sel locations c_{2} -> non empty set ;

sel traces c_{2} -> non empty set ;

sel procE c_{2} -> Function of the processes of c_{2},(bool the carrier of the events of c_{2});

sel traceE c_{2} -> Function of the traces of c_{2},(bool the carrier of the events of c_{2});

sel readE c_{2} -> Function of the locations of c_{2},(bool the carrier of the events of c_{2});

sel writeE c_{2} -> Function of the locations of c_{2},(bool the carrier of the events of c_{2});

sel val_of c_{2} -> PartFunc of the carrier of the events of c_{2}, the carrier of Values;

end;
attr c

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

sel processes c

sel locations c

sel traces c

sel procE c

sel traceE c

sel readE c

sel writeE c

sel val_of c

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

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

end;
let S be Events_structure over Values;

let e be Event of S;

let x be Location of S;

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

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 );

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;

end;
let S be Events_structure over Values;

let x be Location of S;

let E be EventSet of S;

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

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 ) );

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;

end;
let S be Events_structure over Values;

let e be Event of S;

let tr be trace of S;

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

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;

end;
let S be Events_structure over Values;

let e be Event of S;

let p be Process of S;

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

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;

correctness

coherence

the val_of of S . e is object ;

;

end;
let S be Events_structure over Values;

let e be Event of S;

correctness

coherence

the val_of of S . e is object ;

;

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

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;

end;
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;

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

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;

end;
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;

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

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 ) );

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;

end;
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;

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;

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;

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 ) );

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 );

for e being Event of S

for x1, x2 being Location of S holds

( not e reads x1 or not e writesto x2 );

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

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 );

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 );

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 ) ) );

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 ) );

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;

end;
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 );

( S is pr-complete & S is pr-ordered & S is rw-ordered & S is rw-consistent & S is rw-exclusive );

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

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;

existence

ex b_{1} being Events_structure over Values st b_{1} is consistent

end;
existence

ex b

proof end;

definition

let Values be Values_with_Bool;

mode DistributedSysWithSharedMem of Values is consistent Events_structure over Values;

end;
mode DistributedSysWithSharedMem of Values is consistent Events_structure over Values;

definition

let Values be Values_with_Bool;

let DS be DistributedSysWithSharedMem of Values;

let e1, e2 be Event of DS;

end;
let DS be DistributedSysWithSharedMem of Values;

let e1, e2 be Event of DS;

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

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;

coherence

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

end;
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 { e where e is Event of DS : ( e1 < e & e < e2 ) } ;

coherence

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

proof 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 ) } ;

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;

coherence

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

end;
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 { e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } ;

coherence

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

proof 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 ) } ;

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

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 )

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) ;

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;

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

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;

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;

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;

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

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;

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;

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;

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;

end;
let DS be DistributedSysWithSharedMem of Values;

let e1, e2 be Event of DS;

:: simultaneous events

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

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;

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;

end;
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 ) );

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 ) );

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

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 ;

end;
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 ) ) ) );

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 ) ) ) );

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

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 )

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

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;