Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/TLA/Memory/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 11 kB

Quelle Memory.thy Sprache: Isabelle

(*  Title:      HOL/TLA/Memory/Memory.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>RPC-Memory example: Memory specification\<close>

theory Memory
imports MemoryParameters ProcedureInterface
begin

type_synonym memChType = "(memOp, Vals) channel"
type_synonym memType = "(Locs \ Vals) stfun" (* intention: MemLocs \ MemVals *)
type_synonym resType = "(PrIds \ Vals) stfun"

(* state predicates *)

definition MInit :: "memType \ Locs \ stpred"
  where "MInit mm l == PRED mm!l = #InitVal"

definition PInit :: "resType \ PrIds \ stpred"
  where "PInit rs p == PRED rs!p = #NotAResult"

(* auxiliary predicates: is there a pending read/write request for
   some process id and location/value? *)

definition RdRequest :: "memChType \ PrIds \ Locs \ stpred"
  where "RdRequest ch p l == PRED Calling ch p \ (arg = #(read l))"

definition WrRequest :: "memChType \ PrIds \ Locs \ Vals \ stpred"
  where "WrRequest ch p l v == PRED Calling ch p \ (arg = #(write l v))"

(* actions *)

(* a read that doesn't raise BadArg *)
definition GoodRead :: "memType \ resType \ PrIds \ Locs \ action"
  where "GoodRead mm rs p l == ACT #l \ #MemLoc \ ((rs!p)$ = $(mm!l))"

(* a read that raises BadArg *)
definition BadRead :: "memType \ resType \ PrIds \ Locs \ action"
  where "BadRead mm rs p l == ACT #l \ #MemLoc \ ((rs!p)$ = #BadArg)"

(* the read action with l visible *)
definition ReadInner :: "memChType \ memType \ resType \ PrIds \ Locs \ action"
  where "ReadInner ch mm rs p l == ACT
    $(RdRequest ch p l)
    \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
    \<and> unchanged (rtrner ch ! p)"

(* the read action with l quantified *)
definition Read :: "memChType \ memType \ resType \ PrIds \ action"
  where "Read ch mm rs p == ACT (\l. ReadInner ch mm rs p l)"

(* similar definitions for the write action *)
definition GoodWrite :: "memType \ resType \ PrIds \ Locs \ Vals \ action"
  where "GoodWrite mm rs p l v ==
    ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal
      \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"

definition BadWrite :: "memType \ resType \ PrIds \ Locs \ Vals \ action"
  where "BadWrite mm rs p l v == ACT
    \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
    \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"

definition WriteInner :: "memChType \ memType \ resType \ PrIds \ Locs \ Vals \ action"
  where "WriteInner ch mm rs p l v == ACT
    $(WrRequest ch p l v)
    \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
    \<and> unchanged (rtrner ch ! p)"

definition Write :: "memChType \ memType \ resType \ PrIds \ Locs \ action"
  where "Write ch mm rs p l == ACT (\v. WriteInner ch mm rs p l v)"

(* the return action *)
definition MemReturn :: "memChType \ resType \ PrIds \ action"
  where "MemReturn ch rs p == ACT
   (   ($(rs!p) \<noteq> #NotAResult)
    \<and> ((rs!p)$ = #NotAResult)
    \<and> Return ch p (rs!p))"

(* the failure action of the unreliable memory *)
definition MemFail :: "memChType \ resType \ PrIds \ action"
  where "MemFail ch rs p == ACT
    $(Calling ch p)
    \<and> ((rs!p)$ = #MemFailure)
    \<and> unchanged (rtrner ch ! p)"

(* next-state relations for reliable / unreliable memory *)
definition RNext :: "memChType \ memType \ resType \ PrIds \ action"
  where "RNext ch mm rs p == ACT
   (  Read ch mm rs p
    \<or> (\<exists>l. Write ch mm rs p l)
    \<or> MemReturn ch rs p)"

definition UNext :: "memChType \ memType \ resType \ PrIds \ action"
  where "UNext ch mm rs p == ACT (RNext ch mm rs p \ MemFail ch rs p)"

(* temporal formulas *)

definition RPSpec :: "memChType \ memType \ resType \ PrIds \ temporal"
  where "RPSpec ch mm rs p == TEMP
    Init(PInit rs p)
    \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"

definition UPSpec :: "memChType \ memType \ resType \ PrIds \ temporal"
  where "UPSpec ch mm rs p == TEMP
    Init(PInit rs p)
    \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"

definition MSpec :: "memChType \ memType \ resType \ Locs \ temporal"
  where "MSpec ch mm rs l == TEMP
    Init(MInit mm l)
    \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"

definition IRSpec :: "memChType \ memType \ resType \ temporal"
  where "IRSpec ch mm rs == TEMP
    (\<forall>p. RPSpec ch mm rs p)
    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"

definition IUSpec :: "memChType \ memType \ resType \ temporal"
  where "IUSpec ch mm rs == TEMP
    (\<forall>p. UPSpec ch mm rs p)
    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"

definition RSpec :: "memChType \ resType \ temporal"
  where "RSpec ch rs == TEMP (\\mm. IRSpec ch mm rs)"

definition USpec :: "memChType \ temporal"
  where "USpec ch == TEMP (\\mm rs. IUSpec ch mm rs)"

(* memory invariant: in the paper, the invariant is hidden in the definition of
   the predicate S used in the implementation proof, but it is easier to verify
   at this level. *)
definition MemInv :: "memType \ Locs \ stpred"
  where "MemInv mm l == PRED #l \ #MemLoc \ mm!l \ #MemVal"

lemmas RM_action_defs =
  MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
  GoodRead_def BadRead_def ReadInner_def Read_def
  GoodWrite_def BadWrite_def WriteInner_def Write_def
  MemReturn_def RNext_def

lemmas UM_action_defs = RM_action_defs MemFail_def UNext_def

lemmas RM_temp_defs = RPSpec_def MSpec_def IRSpec_def
lemmas UM_temp_defs = UPSpec_def MSpec_def IUSpec_def

(* The reliable memory is an implementation of the unreliable one *)
lemma ReliableImplementsUnReliable: "\ IRSpec ch mm rs \ IUSpec ch mm rs"
  by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)

(* The memory spec implies the memory invariant *)
lemma MemoryInvariant: "\ MSpec ch mm rs l \ \(MemInv mm l)"
  by (auto_invariant simp: RM_temp_defs RM_action_defs)

(* The invariant is trivial for non-locations *)
lemma NonMemLocInvariant: "\ #l \ #MemLoc \ \(MemInv mm l)"
  by (auto simp: MemInv_def intro!: necT [temp_use])

lemma MemoryInvariantAll:
    "\ (\l. #l \ #MemLoc \ MSpec ch mm rs l) \ (\l. \(MemInv mm l))"
  apply clarify
  apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
  done

(* The memory engages in an action for process p only if there is an
   unanswered call from p.
   We need this only for the reliable memory.
*)

lemma Memoryidle: "\ \$(Calling ch p) \ \ RNext ch mm rs p"
  by (auto simp: AReturn_def RM_action_defs)

(* Enabledness conditions *)

lemma MemReturn_change: "\ MemReturn ch rs p \ _(rtrner ch ! p, rs!p)"
  by (force simp: MemReturn_def angle_def)

lemma MemReturn_enabled: "\p. basevars (rtrner ch ! p, rs!p) \
      \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult)
         \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
  apply (tactic
    \<open>action_simp_tac \<^context> [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
  apply (tactic
    \<open>action_simp_tac (\<^context> addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
      @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
  done

lemma ReadInner_enabled: "\p. basevars (rtrner ch ! p, rs!p) \
      \<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)"
  apply (case_tac "l \ MemLoc")
  apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
    intro!: exI elim!: base_enabled [temp_use])+
  done

lemma WriteInner_enabled: "\p. basevars (mm!l, rtrner ch ! p, rs!p) \
      \<turnstile> Calling ch p \<and> (arg<ch!p> = #(write l v))
         \<longrightarrow> Enabled (WriteInner ch mm rs p l v)"
  apply (case_tac "l \ MemLoc \ v \ MemVal")
  apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
    intro!: exI elim!: base_enabled [temp_use])+
  done

lemma ReadResult: "\ Read ch mm rs p \ (\l. $(MemInv mm l)) \ (rs!p)` \ #NotAResult"
  by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)

lemma WriteResult: "\ Write ch mm rs p l \ (rs!p)` \ #NotAResult"
  by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)

lemma ReturnNotReadWrite: "\ (\l. $MemInv mm l) \ MemReturn ch rs p
         \<longrightarrow> \<not> Read ch mm rs p \<and> (\<forall>l. \<not> Write ch mm rs p l)"
  by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])

lemma RWRNext_enabled: "\ (rs!p = #NotAResult) \ (\l. MemInv mm l)
         \<and> Enabled (Read ch mm rs p \<or> (\<exists>l. Write ch mm rs p l))
         \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
  by (force simp: RNext_def angle_def elim!: enabled_mono2
    dest: ReadResult [temp_use] WriteResult [temp_use])

(* Combine previous lemmas: the memory can make a visible step if there is an
   outstanding call for which no result has been produced.
*)
lemma RNext_enabled: "\p. \l. basevars (mm!l, rtrner ch!p, rs!p) \
      \<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l)
         \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
  apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
  apply (case_tac "arg (ch w p)")
   apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Read_def},
     temp_rewrite \<^context> @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>)
   apply (force dest: base_pair [temp_use])
  apply (erule contrapos_np)
  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Write_def},
    temp_rewrite \<^context> @{thm enabled_ex}])
    [@{thm WriteInner_enabled}, exI] [] 1\<close>)
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

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.