Quelle Token.thy

Sprache: Isabelle

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

section ‹The Token Ring›

theory Token
imports "../WFair"

begin

text‹From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.›

subsection‹Definitions›

datatype pstate = Hungry | Eating | Thinking
    🍋 ‹process states›

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‹Progress under Weak Fairness›

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 (cases ‹i 🚫›)
   apply (auto simp add: nodeOrder_def next_def mod_Suc add.commute [of _ N])
  apply (simp only: diff_add_assoc mod_add_self1)
  apply simp
  done

text‹From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of ‹cases›. Reasoning about leadsTo takes practice!›
lemma TR7_nodeOrder:
     "[| i
      F ∈ (HasTok i) leadsTo ({s. (token s, i) ∈ nodeOrder j} ∪ 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‹Chapter 4 variant, the one actually used below.›
lemma TR7_aux: "[| i≠j |]
      ==> F ∈ (HasTok i) leadsTo {s. (token s, i) ∈ 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‹Misra's TR9: the token reaches an arbitrary node›
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‹Misra's TR8: a hungry process eventually eats›
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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-05-03) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.