Quelle Deadlock.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/Deadlock.thy
    Author:     Olaf Müller
*)

section \<open>Deadlock freedom of I/O Automata\<close>

theory Deadlock
imports RefCorrectness CompoScheds
begin

text \<open>Input actions may always be added to a schedule.\<close>

lemma scheds_input_enabled:
  "Filter (\x. x \ act A) \ sch \ schedules A \ a \ inp A \ input_enabled A \ Finite sch
    \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) \<cdot> sch @@ a \<leadsto> nil \<in> schedules A"
  apply (simp add: schedules_def has_schedule_def)
  apply auto
  apply (frule inp_is_act)
  apply (simp add: executions_def)
  apply (pair ex)
  apply (rename_tac s ex)
  apply (subgoal_tac "Finite ex")
  prefer 2
  apply (simp add: filter_act_def)
  defer
  apply (rule_tac [2] Map2Finite [THEN iffD1])
  apply (rule_tac [2] t = "Map fst \ ex" in subst)
  prefer 2
  apply assumption
  apply (erule_tac [2] FiniteFilter)
  text \<open>subgoal 1\<close>
  apply (frule exists_laststate)
  apply (erule allE)
  apply (erule exE)
  text \<open>using input-enabledness\<close>
  apply (simp add: input_enabled_def)
  apply (erule conjE)+
  apply (erule_tac x = "a" in allE)
  apply simp
  apply (erule_tac x = "u" in allE)
  apply (erule exE)
  text \<open>instantiate execution\<close>
  apply (rule_tac x = " (s, ex @@ (a, s2) \ nil) " in exI)
  apply (simp add: filter_act_def MapConc)
  apply (erule_tac t = "u" in lemma_2_1)
  apply simp
  apply (rule sym)
  apply assumption
  done

text \<open>
  Deadlock freedom: component B cannot block an out or int action of component
  A in every schedule.

  Needs compositionality on schedule level, input-enabledness, compatibility
  and distributivity of \<open>is_exec_frag\<close> over \<open>@@\<close>.
\<close>

lemma IOA_deadlock_free:
  assumes "a \ local A"
    and "Finite sch"
    and "sch \ schedules (A \ B)"
    and "Filter (\x. x \ act A) \ (sch @@ a \ nil) \ schedules A"
    and "compatible A B"
    and "input_enabled B"
  shows "(sch @@ a \ nil) \ schedules (A \ B)"
  supply if_split [split del]
  apply (insert assms)
  apply (simp add: compositionality_sch locals_def)
  apply (rule conjI)
  text \<open>\<open>a \<in> act (A \<parallel> B)\<close>\<close>
  prefer 2
  apply (simp add: actions_of_par)
  apply (blast dest: int_is_act out_is_act)

  text \<open>\<open>Filter B (sch @@ [a]) \<in> schedules B\<close>\<close>
  apply (case_tac "a \ int A")
  apply (drule intA_is_not_actB)
  apply (assumption) (* \<longrightarrow> a \<notin> act B *)
  apply simp

  text \<open>case \<open>a \<notin> int A\<close>, i.e. \<open>a \<in> out A\<close>\<close>
  apply (case_tac "a \ act B")
  apply simp
  text \<open>case \<open>a \<in> act B\<close>\<close>
  apply simp
  apply (subgoal_tac "a \ out A")
  prefer 2
  apply blast
  apply (drule outAactB_is_inpB)
  apply assumption
  apply assumption
  apply (rule scheds_input_enabled)
  apply simp
  apply assumption+
  done

end

quality98%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

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 ist noch experimentell.