Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Token.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/Simple/Token.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section \<open>The Token Ring\<close>

theory Token
imports "../WFair"

begin

text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close>

subsection\<open>Definitions\<close>

datatype pstate = Hungry | Eating | Thinking
    \<comment> \<open>process states\<close>

record state =
  token :: "nat"
  proc  :: "nat => pstate"

definition HasTok :: "nat => state set" where
    "HasTok i == {s. token s = i}"

definition H :: "nat => state set" where
    "H i == {s. proc s i = Hungry}"

definition E :: "nat => state set" where
    "E i == {s. proc s i = Eating}"

definition T :: "nat => state set" where
    "T i == {s. proc s i = Thinking}"

locale Token =
  fixes N and F and nodeOrder and "next"
  defines nodeOrder_def:
       "nodeOrder j == measure(%i. ((j+N)-i) mod N) \ {.. {..
      and next_def:
       "next i == (Suc i) mod N"
  assumes N_positive [iff]: "0
      and TR2:  "F \ (T i) co (T i \ H i)"
      and TR3:  "F \ (H i) co (H i \ E i)"
      and TR4:  "F \ (H i - HasTok i) co (H i)"
      and TR5:  "F \ (HasTok i) co (HasTok i \ -(E i))"
      and TR6:  "F \ (H i \ HasTok i) leadsTo (E i)"
      and TR7:  "F \ (HasTok i) leadsTo (HasTok (next i))"

lemma HasToK_partition: "[| s \ HasTok i; s \ HasTok j |] ==> i=j"
by (unfold HasTok_def, auto)

lemma not_E_eq: "(s \ E i) = (s \ H i | s \ T i)"
apply (simp add: H_def E_def T_def)
apply (cases "proc s i", auto)
done

context Token
begin

lemma token_stable: "F \ stable (-(E i) \ (HasTok i))"
apply (unfold stable_def)
apply (rule constrains_weaken)
apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
apply (auto simp add: not_E_eq)
apply (simp_all add: H_def E_def T_def)
done

subsection\<open>Progress under Weak Fairness\<close>

lemma wf_nodeOrder: "wf(nodeOrder j)"
apply (unfold nodeOrder_def)
apply (rule wf_measure [THEN wf_subset], blast)
done

lemma nodeOrder_eq:
     "[| i ((next i, i) \ nodeOrder j) = (i \ j)"
apply (unfold nodeOrder_def next_def)
apply (auto simp add: mod_Suc mod_geq)
apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
done

text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
  Note the use of \<open>cases\<close>.  Reasoning about leadsTo takes practice!\<close>
lemma TR7_nodeOrder:
     "[| i
      F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
apply (cases "i=j")
apply (blast intro: subset_imp_leadsTo)
apply (rule TR7 [THEN leadsTo_weaken_R])
apply (auto simp add: HasTok_def nodeOrder_eq)
done

text\<open>Chapter 4 variant, the one actually used below.\<close>
lemma TR7_aux: "[| ij |]
      ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
apply (rule TR7 [THEN leadsTo_weaken_R])
apply (auto simp add: HasTok_def nodeOrder_eq)
done

lemma token_lemma:
     "({s. token s < N} \ token -` {m}) = (if m
by auto

text\<open>Misra's TR9: the token reaches an arbitrary node\<close>
lemma leadsTo_j: "j F \ {s. token s < N} leadsTo (HasTok j)"
apply (rule leadsTo_weaken_R)
apply (rule_tac I = "-{j}" and f = token and B = "{}"
       in wf_nodeOrder [THEN bounded_induct])
apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
prefer 2 apply blast
apply clarify
apply (rule TR7_aux [THEN leadsTo_weaken])
apply (auto simp add: HasTok_def nodeOrder_def)
done

text\<open>Misra's TR8: a hungry process eventually eats\<close>
lemma token_progress:
     "j F \ ({s. token s < N} \ H j) leadsTo (E j)"
apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
apply (rule_tac [2] TR6)
apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
done

end

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.