(* Algorithme d'exclusion mutuelle de Peterson. *) Require PolyList. Require Bool. Require Arith. Require ZArith. (* On a deux processus, nommes 1 et 2. Le but est de montrer que, partant chacun de l'etat NonCritique, les deux processus ne se retrouvent jamais tous les deux en meme temps en section critique, c'est-a-dire dans l'etat Critique. Ceci permet aux deux processus 1 et 2 en parallele de se partager une ressource en etant sur que l'autre processus n'est pas en train de la modifier. L'algorithme de Peterson est realise a l'aide de trois variables : - c1 est un booleen que le processus 1 peut lire et ecrire, et que le processus 2 ne peut que lire (atomiquement); il est initialement vrai. - c2 est un booleen que le processus 2 peut lire et ecrire, et que le processus 1 ne peut que lire (atomiquement); il est initialement vrai. - tour est un booleen, valant faux (=processus 1) ou vrai (=processus 2), et que les deux processus peuvent lire et ecrire de facon atomique (sans etre interrompu par l'autre processus). *) (* En graphiques (les noms entre crochets sont des etats, les fleches sont les transitions): Processus 1: Processus 2: ______________ ______________ / \ / \ / \ / \ L \ L \ [NonCritique] \ [NonCritique] \ | \ | \ c1:=true \ c2:=true \ | | | | v | v | [Pose] | [Pose] | | | | | tour:=true__ | tour:=false_ | | / \ | | / \ | v L (si c2=true | v L (si c1=true | [Attente] et tour=true) | [Attente] et tour=faux) | | \_____/ | | \_____/ | (si c2=false / (si c1=false / ou tour=false) / ou tour=true) / | / | / v / v / [Critique] / [Critique] / | / | / c1:=false / c2:=false / \ / \ / \___________/ \___________/ Le but est de montrer que, partant de l'etat NonCritique pour chaque processus, avec c1=c2=true, on ne peut jamais arriver dans l'etat ou les deux processus sont dans l'etat Critique en meme temps. *) Inductive pc : Set := (* le compteur de programme de chaque processus. *) NonCritique : pc | Critique : pc | Pose : pc | Attente : pc. Definition proc := bool. (* le type des processus, peut etre faux (=1) ou vrai (=2). *) Inductive etat : Set := Etat : bool -> bool -> pc -> pc -> proc -> etat (* c1 c2 pc1 pc2 tour *) . (* Etat : (proc -> bool) -> (proc -> pc) -> proc -> etat (* ^- pour chaque ^- pour chaque ^- la valeur de processus i, processus i, la variable la valeur de la valeur pc(i) partagee tour. c(i). de son compteur de programme. *) . *) Lemma choix_bool : (b:bool) b=true \/ b=false. Proof. Induction b. Left . Reflexivity. Right . Reflexivity. Qed. Inductive transition : etat -> etat -> Prop := prepare1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 NonCritique pc2 tour) (Etat true c2 Pose pc2 tour)) (* Processus 1 fait : [NonCritique] c1:=true [Pose] *) | prepare2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 NonCritique tour) (Etat c1 true pc1 Pose tour)) (* Processus 2 fait : [NonCritique] c2:=true [Pose] *) | pose1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 Pose pc2 tour) (Etat c1 c2 Attente pc2 true)) (* Processus 1 fait : [Pose] tour:=true [Attente] *) | pose2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 Pose tour) (Etat c1 c2 pc1 Attente false)) (* Processus 2 fait : [Pose] tour:=false [Attente] *) | attente1 : (c1,c2:bool) (pc2:pc) (tour:proc) c2=true /\ tour=true -> (transition (Etat c1 c2 Attente pc2 tour) (Etat c1 c2 Attente pc2 tour)) (* Processus 1 fait : si c2 vrai et tour vrai, [Attente] nop [Attente] *) | attente2 : (c1,c2:bool) (pc1:pc) (tour:proc) c1=true /\ tour=false -> (transition (Etat c1 c2 pc1 Attente tour) (Etat c1 c2 pc1 Attente tour)) (* Processus 2 fait : si c1 vrai et tour faux, [Attente] nop [Attente] *) | entre1 : (c1,c2:bool) (pc2:pc) (tour:proc) c2=false \/ tour=false -> (transition (Etat c1 c2 Attente pc2 tour) (Etat c1 c2 Critique pc2 tour)) (* Processus 1 fait : si c2 faux ou tour faux, [Attente] nop [Critique] *) | entre2 : (c1,c2:bool) (pc1:pc) (tour:proc) c1=false \/ tour=true -> (transition (Etat c1 c2 pc1 Attente tour) (Etat c1 c2 pc1 Critique tour)) (* Processus 2 fait : si c1 faux ou tour vrai, [Attente] nop [Critique] *) | sort1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 Critique pc2 tour) (Etat false c2 NonCritique pc2 tour)) (* Processus 1 fait : [Critique] c1:=false [NonCritique] *) | sort2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 Critique tour) (Etat c1 false pc1 NonCritique tour)) (* Processus 2 fait : [Critique] c1:=false [NonCritique] *) . Inductive exec : etat -> etat -> Prop := nop : (s1,s2:etat) s1=s2 -> (exec s1 s2) (* On peut aller de s1 a s2 en ne faisant rien, mais alors s1=s2. *) | qqch : (s1,s2,s3:etat) (exec s1 s2) -> (transition s2 s3) -> (exec s1 s3). (* Ou on peut faire une execution pour aller de s1 a s2, puis faire une etape de s2 a s3. Ceci definit une execution (non vide) de s1 a s3. *) (* On montre d'abord que quand le processus 1 est dans l'etat Pose, ou l'etat Attente, ou l'etat Critique, necessairement c1 est vrai: *) Lemma apres_prepare_c1_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Pose \/ pc1=Attente \/ pc1=Critique -> c1=true. (* Donc quand le processus 1 est en section critique (dans l'etat Critique), c1 vaut true: *) Lemma en_critique_c1_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Critique -> c1=true. (* On montre ensuite le lemme analogue que quand le processus 2 est dans l'etat Pose, ou l'etat Attente, ou l'etat Critique, necessairement c2 est vrai: *) Lemma apres_prepare_c2_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Pose \/ pc2=Attente \/ pc2=Critique -> c2=true. (* Donc quand le processus 2 est en section critique (dans l'etat Critique), c2 vaut true: *) Lemma en_critique_c2_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Critique -> c2=true. Lemma en_critique1_tour_est_faux : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Critique -> ~pc2=Pose -> c2=true -> tour=false. Lemma en_critique2_tour_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Critique -> ~pc1=Pose -> c1=true -> tour=true. Lemma exclusion_mutuelle : (s0,s:etat) (exec s0 s) -> (tour0,tour:proc) (c1,c2:bool) s0=(Etat true true NonCritique NonCritique tour0) -> ~s =(Etat c1 c2 Critique Critique tour). (* Il n'est pas possible, partant d'un etat initial ou c1=c2=true, pc1=pc2=NonCritique, d'arriver a un etat ou les deux processus sont en section critique en meme temps (pc1=pc2=Critique). *)