diff --git a/thys/ConcurrentIMP/CIMP.thy b/thys/ConcurrentIMP/CIMP.thy --- a/thys/ConcurrentIMP/CIMP.thy +++ b/thys/ConcurrentIMP/CIMP.thy @@ -1,134 +1,40 @@ (*<*) (* * Copyright 2015, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) theory CIMP imports CIMP_pred CIMP_lang CIMP_vcg - "HOL-Library.Sublist" + CIMP_vcg_rules keywords - "inv_definition" "locset_definition" :: thy_defn + "locset_definition" :: thy_defn + and "intern_com" :: thy_decl begin text\ Infrastructure for reasoning about CIMP programs. See AFP entry \ConcurrentGC\ for examples of use. \ -named_theorems com "Command definitions" -named_theorems inv "Location-sensitive invariant definitions" -named_theorems loc "Location set membership cache" - -ML\ - -signature CIMP = -sig - val com_locs_fold : (term -> 'b -> 'b) -> 'b -> term -> 'b - val com_locs_map : (term -> 'b) -> term -> 'b list - val com_locs_fold_no_response : (term -> 'b -> 'b) -> 'b -> term -> 'b - val com_locs_map_no_response : (term -> 'b) -> term -> 'b list - val def_inv : thm -> local_theory -> local_theory - val def_locset : thm -> local_theory -> local_theory -end; - -structure Cimp : CIMP = -struct - -fun com_locs_fold f x (Const (@{const_name Request}, _) $ l $ _ $ _ ) = f l x - | com_locs_fold f x (Const (@{const_name Response}, _) $ l $ _) = f l x - | com_locs_fold f x (Const (@{const_name LocalOp}, _) $ l $ _) = f l x - | com_locs_fold f x (Const (@{const_name Cond1}, _) $ l $ _ $ c) = com_locs_fold f (f l x) c - | com_locs_fold f x (Const (@{const_name Cond2}, _) $ l $ _ $ c1 $ c2) = com_locs_fold f (com_locs_fold f (f l x) c1) c2 - | com_locs_fold f x (Const (@{const_name Loop}, _) $ c) = com_locs_fold f x c - | com_locs_fold f x (Const (@{const_name While}, _) $ l $ _ $ c) = com_locs_fold f (f l x) c - | com_locs_fold f x (Const (@{const_name Seq}, _) $ c1 $ c2) = com_locs_fold f (com_locs_fold f x c1) c2 - | com_locs_fold f x (Const (@{const_name Choose}, _) $ c1 $ c2) = com_locs_fold f (com_locs_fold f x c1) c2 - | com_locs_fold _ x _ = x; - -fun com_locs_map f com = com_locs_fold (fn l => fn acc => f l :: acc) [] com - -fun com_locs_fold_no_response f x (Const (@{const_name Request}, _) $ l $ _ $ _ ) = f l x - | com_locs_fold_no_response _ x (Const (@{const_name Response}, _) $ _ $ _) = x (* can often ignore \Response\ *) - | com_locs_fold_no_response f x (Const (@{const_name LocalOp}, _) $ l $ _) = f l x - | com_locs_fold_no_response f x (Const (@{const_name Cond1}, _) $ l $ _ $ c) = com_locs_fold_no_response f (f l x) c - | com_locs_fold_no_response f x (Const (@{const_name Cond2}, _) $ l $ _ $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f (f l x) c1) c2 - | com_locs_fold_no_response f x (Const (@{const_name Loop}, _) $ c) = com_locs_fold_no_response f x c - | com_locs_fold_no_response f x (Const (@{const_name While}, _) $ l $ _ $ c) = com_locs_fold_no_response f (f l x) c - | com_locs_fold_no_response f x (Const (@{const_name Seq}, _) $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2 - | com_locs_fold_no_response f x (Const (@{const_name Choose}, _) $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2 - | com_locs_fold_no_response _ x _ = x; - -fun com_locs_map_no_response f com = com_locs_fold_no_response (fn l => fn acc => f l :: acc) [] com - -(* Cache location set membership facts. - -Decide membership in the given set for each label in the CIMP programs -in the Named_Theorems "com". +named_theorems locset_cache "Location set membership cache" -If the label set and com types differ, we probably get a nasty error. - -*) +lemmas cleanup_simps = + atomize_eq + simp_thms -fun def_locset thm ctxt = - let - val set_name = thm - |> Local_Defs.meta_rewrite_rule ctxt (* handle `=` or `\` *) - |> Thm.cprop_of |> Thm.dest_equals |> fst |> Thm.term_of - val set_typ = set_name |> type_of - val elt_typ = case set_typ of Type ("Set.set", [t]) => t | _ => raise Fail "thm should define a set" - val set_name_str = case set_name of Const (c, _) => c | Free (c, _) => c | _ => error ("Not an equation of the form x = set: " ^ Thm.string_of_thm ctxt thm) - val thm_name = Binding.qualify true set_name_str (Binding.name "memb") - fun mk_memb l = Thm.cterm_of ctxt (Const (@{const_name "Set.member"}, elt_typ --> set_typ --> @{typ "bool"}) $ l $ set_name) - val rewrite_tac = Simplifier.rewrite (ctxt addsimps ([thm] @ Named_Theorems.get ctxt @{named_theorems "loc"})) (* probably want the ambient simpset + some stuff *) - val coms = Named_Theorems.get ctxt @{named_theorems "com"} |> map (Thm.cprop_of #> Thm.dest_equals #> snd #> Thm.term_of) - val attrs = [(* Attrib.internal (K (Clasimp.iff_add)), *) Attrib.internal (K (Named_Theorems.add @{named_theorems "loc"}))] -(* Parallel *) - fun mk_thms coms = Par_List.map rewrite_tac (maps (com_locs_map_no_response mk_memb) coms) -(* Sequential *) -(* fun mk_thms coms = List.foldl (fn (c, thms) => com_locs_fold (fn l => fn thms => rewrite_tac (mk_memb l) :: thms) thms c) [] coms *) - in - ctxt - |> Local_Theory.note ((thm_name, attrs), mk_thms coms) - |> snd - end; - -(* FIXME later need to rewrite using interned labels (fold defs). *) -fun def_inv thm ctxt : local_theory = - let - val attrs = [Attrib.internal (K (Named_Theorems.add @{named_theorems "inv"}))] - in - ctxt - |> Local_Theory.note ((Binding.empty, attrs), [thm]) - |> snd - end; - -end; - -val _ = - Outer_Syntax.local_theory' \<^command_keyword>\inv_definition\ "constant definition for invariants" - (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- - Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy => - Specification.definition_cmd decl params prems spec b lthy - |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_inv)); - -val _ = - Outer_Syntax.local_theory' \<^command_keyword>\locset_definition\ "constant definition for sets of locations" - (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- - Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy => - Specification.definition_cmd decl params prems spec b lthy - |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_locset)); -\ +ML_file\cimp.ML\ +(*<*) end (*>*) diff --git a/thys/ConcurrentIMP/CIMP_lang.thy b/thys/ConcurrentIMP/CIMP_lang.thy --- a/thys/ConcurrentIMP/CIMP_lang.thy +++ b/thys/ConcurrentIMP/CIMP_lang.thy @@ -1,946 +1,510 @@ (*<*) (* * Copyright 2015, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) theory CIMP_lang imports CIMP_pred + LTL begin (*>*) -section\CIMP syntax and semantics\ +section\CIMP syntax and semantics \label{sec:cimp-syntax-semantics}\ text\ -\label{sec:cimp-syntax-semantics} - We define a small sequential programming language with synchronous message passing primitives for describing the individual processes. This has the advantage over raw transition systems in that it is programmer-readable, includes sequential composition, supports a program logic and VCG (\S\ref{sec:cimp-vcg}), etc. These processes are composed in parallel at the top-level. CIMP is inspired by IMP, as presented by @{cite [cite_macro=citet] "Winskel:1993"} and @{cite [cite_macro=citet] "ConcreteSemantics:2014"}, and the classical process algebras CCS @{cite [cite_macro=citep] "Milner:1980" and "Milner:1989"} and CSP @{cite [cite_macro=citep] "Hoare:1985"}. Note that the algebraic properties of this language have not been developed. As we operate in a concurrent setting, we need to provide a small-step semantics (\S\ref{sec:cimp-semantics}), which we give in the style of \emph{structural operational semantics} (SOS) as popularised by @{cite [cite_macro=citet] "DBLP:journals/jlp/Plotkin04"}. The semantics of a complete system (\S\ref{sec:cimp-system-steps}) is presently taken simply to be the states reachable by interleaving the enabled steps of the individual processes, subject to message passing rendezvous. We leave a trace or branching semantics to future work. +This theory contains all the trusted definitions. The soundness of the other +theories supervenes upon this one. + \ + subsection\Syntax\ text\ Programs are represented using an explicit (deep embedding) of their syntax, as the semantics needs to track the progress of multiple threads of control. Each (atomic) \emph{basic command} (\S\ref{sec:cimp-decompose}) is annotated with a @{typ "'location"}, which we use in our assertions (\S\ref{sec:cimp-control-predicates}). These locations need not be unique, though in practice they likely will be. Processes maintain \emph{local states} of type @{typ "'state"}. These can be updated with arbitrary relations of @{typ "'state \ 'state set"} with \LocalOp\, and conditions of type @{typ "'s \ bool"} are similarly shallowly embedded. This arrangement allows the end-user to select their own level of atomicity. The sequential composition operator and control constructs are standard. We add the infinite looping construct \Loop\ so we can construct single-state reactive systems; this has implications for fairness assertions. \ type_synonym 's bexp = "'s \ bool" datatype ('answer, 'location, 'question, 'state) com = Request "'location" "'state \ 'question" "'answer \ 'state \ 'state set" ("\_\ Request _ _" [0, 70, 70] 71) | Response "'location" "'question \ 'state \ ('state \ 'answer) set" ("\_\ Response _" [0, 70] 71) | LocalOp "'location" "'state \ 'state set" ("\_\ LocalOp _" [0, 70] 71) - | Cond1 "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" ("\_\ IF _ THEN _ FI" [0, 0] 71) + | Cond1 "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" ("\_\ IF _ THEN _ FI" [0, 0, 0] 71) | Cond2 "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" - "('answer, 'location, 'question, 'state) com" ("\_\ IF _/ THEN _/ ELSE _/ FI" [0, 0, 0] 71) + "('answer, 'location, 'question, 'state) com" ("\_\ IF _/ THEN _/ ELSE _/ FI" [0, 0, 0, 0] 71) | Loop "('answer, 'location, 'question, 'state) com" ("LOOP DO _/ OD" [0] 71) | While "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" ("\_\ WHILE _/ DO _/ OD" [0, 0, 0] 71) | Seq "('answer, 'location, 'question, 'state) com" "('answer, 'location, 'question, 'state) com" (infixr ";;" 69) | Choose "('answer, 'location, 'question, 'state) com" - "('answer, 'location, 'question, 'state) com" (infixl "\" 68) + "('answer, 'location, 'question, 'state) com" (infixl "\" 68) text\ We provide a one-armed conditional as it is the common form and avoids the need to discover a label for an internal \SKIP\ and/or trickier proofs about the VCG. In contrast to classical process algebras, we have local state and -distinct send and receive actions. These provide an interface to +distinct request and response actions. These provide an interface to Isabelle/HOL's datatypes that avoids the need for binding (ala the $\pi$-calculus of @{cite [cite_macro=citet] "Milner:1989"}) or large non-deterministic sums (ala CCS @{cite [cite_macro=citep] \\S2.8\ -"Milner:1980"}). Intuitively the sender asks a @{typ "'question"} with +"Milner:1980"}). Intuitively the requester poses a @{typ "'question"} with a \Request\ command, which upon rendezvous with a -receiver's \Response\ command receives an @{typ +responder's \Response\ command receives an @{typ "'answer"}. The @{typ "'question"} is a deterministic function of the -sender's local state, whereas a receiver can respond -non-deterministically. Note that CIMP does not provide a notion of +requester's local state, whereas responses can be +non-deterministic. Note that CIMP does not provide a notion of channel; these can be modelled by a judicious choice of @{typ "'question"}. -We also provide a binary external choice operator. Internal choice can -be recovered in combination with local operations (see @{cite -[cite_macro=citet] \\S2.3\ "Milner:1980"}). +We also provide a binary external choice operator @{term\Choose\} (infix @{term\(\)\}). +Internal choice can be recovered in combination with local operations +(see @{cite [cite_macro=citet] \\S2.3\ "Milner:1980"}). We abbreviate some common commands: \SKIP\ is a local operation that does nothing, and the floor brackets simplify deterministic \LocalOp\s. We also adopt some syntax magic from -Makarius's Hoare and Multiquote theories in the Isabelle/HOL +Makarius's \Hoare\ and \Multiquote\ theories in the Isabelle/HOL distribution. \ -abbreviation SKIP_syn ("\_\/ SKIP" 70) where +abbreviation SKIP_syn ("\_\/ SKIP" [0] 71) where "\l\ SKIP \ \l\ LocalOp (\s. {s})" abbreviation (input) DetLocalOp :: "'location \ ('state \ 'state) - \ ('answer, 'location, 'question, 'state) com" ("\_\ \_\") where + \ ('answer, 'location, 'question, 'state) com" ("\_\ \_\" [0, 0] 71) where "\l\ \f\ \ \l\ LocalOp (\s. {f s})" syntax "_quote" :: "'b \ ('a \ 'b)" ("\_\" [0] 1000) "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) - "_Assign" :: "'location \ idt \ 'b \ ('answer, 'location, 'question, 'state) com" ("(\_\ \_ :=/ _)" [0, 0, 70] 71) (* FIXME precedence -- see massive ambiguities in the GC model *) + "_Assign" :: "'location \ idt \ 'b \ ('answer, 'location, 'question, 'state) com" ("(\_\ \_ :=/ _)" [0, 0, 70] 71) "_NonDetAssign" :: "'location \ idt \ 'b set \ ('answer, 'location, 'question, 'state) com" ("(\_\ \_ :\/ _)" [0, 0, 70] 71) abbreviation (input) NonDetAssign :: "'location \ (('val \ 'val) \ 'state \ 'state) \ ('state \ 'val set) \ ('answer, 'location, 'question, 'state) com" where "NonDetAssign l upd es \ \l\ LocalOp (\s. { upd \e\ s |e. e \ es s })" translations "\l\ \x := e" => "CONST DetLocalOp l \\(_update_name x (\_. e))\" "\l\ \x :\ es" => "CONST NonDetAssign l (_update_name x) \es\" parse_translation \ let fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) = antiquote_tr i t $ Bound i | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t) | antiquote_tr _ a = a and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) = c $ skip_antiquote_tr i t | skip_antiquote_tr i t = antiquote_tr i t; fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t)) | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, K quote_tr)] end \ -subsection\Process semantics\ +subsection\Process semantics \label{sec:cimp-semantics} \ text\ -\label{sec:cimp-semantics} - Here we define the semantics of a single process's program. We begin by defining the type of externally-visible behaviour: \ datatype ('answer, 'question) seq_label = sl_Internal ("\") | sl_Send 'question 'answer ("\_, _\") | sl_Receive 'question 'answer ("\_, _\") text\ We define a \emph{labelled transition system} (an LTS) using an execution-stack style of semantics that avoids special treatment of the \SKIP\s introduced by a traditional small step semantics (such as @{cite [cite_macro=citet] \Chapter~14\ "Winskel:1993"}) when a basic command is executed. This was suggested by Thomas Sewell; @{cite [cite_macro=citet] "PittsAM:opespe"} gave a semantics to an ML-like language using this approach. +We record the location of the command that was executed to support +fairness constraints. + \ type_synonym ('answer, 'location, 'question, 'state) local_state - = "('answer, 'location, 'question, 'state) com list \ 'state" + = "('answer, 'location, 'question, 'state) com list \ 'location option \ 'state" inductive small_step :: "('answer, 'location, 'question, 'state) local_state \ ('answer, 'question) seq_label \ ('answer, 'location, 'question, 'state) local_state \ bool" ("_ \\<^bsub>_\<^esub> _" [55, 0, 56] 55) where - Request: "\ \ = action s; s' \ val \ s \ \ (\l\ Request action val # cs, s) \\<^bsub>\\, \\\<^esub> (cs, s')" -| Response: "(s', \) \ action \ s \ (\l\ Response action # cs, s) \\<^bsub>\\, \\\<^esub> (cs, s')" - -| LocalOp: "s' \ R s \ (\l\ LocalOp R # cs, s) \\<^bsub>\\<^esub> (cs, s')" - -| Cond1True: "b s \ (\l\ IF b THEN c FI # cs, s) \\<^bsub>\\<^esub> (c # cs, s)" -| Cond1False: "\b s \ (\l\ IF b THEN c FI # cs, s) \\<^bsub>\\<^esub> (cs, s)" + "\ \ = action s; s' \ val \ s \ \ (\l\ Request action val # cs, _, s) \\<^bsub>\\, \\\<^esub> (cs, Some l, s')" +| "(s', \) \ action \ s \ (\l\ Response action # cs, _, s) \\<^bsub>\\, \\\<^esub> (cs, Some l, s')" -| Cond2True: "b s \ (\l\ IF b THEN c1 ELSE c2 FI # cs, s) \\<^bsub>\\<^esub> (c1 # cs, s)" -| Cond2False: "\b s \ (\l\ IF b THEN c1 ELSE c2 FI # cs, s) \\<^bsub>\\<^esub> (c2 # cs, s)" - -| Loop: "(c # LOOP DO c OD # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (LOOP DO c OD # cs, s) \\<^bsub>\\<^esub> (cs', s')" +| "s' \ R s \ (\l\ LocalOp R # cs, _, s) \\<^bsub>\\<^esub> (cs, Some l, s')" -| While: "b s \ (\l\ WHILE b DO c OD # cs, s) \\<^bsub>\\<^esub> (c # \l\ WHILE b DO c OD # cs, s)" -| WhileFalse: "\ b s \ (\l\ WHILE b DO c OD # cs, s) \\<^bsub>\\<^esub> (cs, s)" +| "b s \ (\l\ IF b THEN c FI # cs, _, s) \\<^bsub>\\<^esub> (c # cs, Some l, s)" +| "\b s \ (\l\ IF b THEN c FI # cs, _, s) \\<^bsub>\\<^esub> (cs, Some l, s)" -| Seq: "(c1 # c2 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1;; c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" +| "b s \ (\l\ IF b THEN c1 ELSE c2 FI # cs, _, s) \\<^bsub>\\<^esub> (c1 # cs, Some l, s)" +| "\b s \ (\l\ IF b THEN c1 ELSE c2 FI # cs, _, s) \\<^bsub>\\<^esub> (c2 # cs, Some l, s)" -| Choose1: "(c1 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1 \ c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" -| Choose2: "(c2 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1 \ c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" +| "(c # LOOP DO c OD # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (LOOP DO c OD # cs, s) \\<^bsub>\\<^esub> (cs', s')" + +| "b s \ (\l\ WHILE b DO c OD # cs, _, s) \\<^bsub>\\<^esub> (c # \l\ WHILE b DO c OD # cs, Some l, s)" +| "\ b s \ (\l\ WHILE b DO c OD # cs, _, s) \\<^bsub>\\<^esub> (cs, Some l, s)" + +| "(c1 # c2 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1;; c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" + +| Choose1: "(c1 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1 \ c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" +| Choose2: "(c2 # cs, s) \\<^bsub>\\<^esub> (cs', s') \ (c1 \ c2 # cs, s) \\<^bsub>\\<^esub> (cs', s')" text\ -The following projections operate on local states. These are internal -to CIMP and should not appear to the end-user. +The following projections operate on local states. These should not +appear to the end-user. \ abbreviation cPGM :: "('answer, 'location, 'question, 'state) local_state \ ('answer, 'location, 'question, 'state) com list" where "cPGM \ fst" -abbreviation cLST :: "('answer, 'location, 'question, 'state) local_state \ 'state" where - "cLST s \ snd s" -(*<*) - -declare small_step.intros[intro] - -inductive_cases small_step_inv[elim]: - "(\l\ Request action val # cs, ls) \\<^bsub>a\<^esub> s'" - "(\l\ Response action # cs, ls) \\<^bsub>a\<^esub> s'" - "(\l\ LocalOp R # cs, ls) \\<^bsub>a\<^esub> s'" - "(\l\ IF b THEN c FI # cs, ls) \\<^bsub>a\<^esub> s'" - "(\l\ IF b THEN c1 ELSE c2 FI # cs, ls) \\<^bsub>a\<^esub> s'" - "(\l\ WHILE b DO c OD # cs, ls) \\<^bsub>a\<^esub> s'" - "(LOOP DO c OD # cs, ls) \\<^bsub>a\<^esub> s'" - -lemma small_step_impossible[iff]: - "\(\l\ Request action val # cs, ls) \\<^bsub>\\<^esub> s'" - "\(\l\ Request action val # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ Response action' # cs, ls) \\<^bsub>\\<^esub> s'" - "\(\l\ Response action' # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ LocalOp R # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ LocalOp R # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ IF b THEN c FI # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ IF b THEN c FI # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ IF b THEN c1 ELSE c2 FI # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ IF b THEN c1 ELSE c2 FI # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ WHILE b DO c OD # cs, ls) \\<^bsub>\\, \\\<^esub> s'" - "\(\l\ WHILE b DO c OD # cs, ls) \\<^bsub>\\, \\\<^esub> s'" -by (auto elim: small_step.cases) - -lemma small_step_stuck[iff]: - "\ ([], l, s) \\<^bsub>\\<^esub> c'" -by (auto elim: small_step.cases) - -(*>*) -text\ - -\label{sec:cimp-decompose} - -To reason about system transitions we need to identify which basic -statement gets executed next. To that end we factor out the recursive -cases of the @{term "small_step"} semantics into \emph{contexts}, -which identify the \basic_com\ commands with immediate -externally-visible behaviour. Note that non-determinism means that -more than one \basic_com\ can be enabled at a time. - -The representation of evaluation contexts follows @{cite -[cite_macro=citet] "DBLP:journals/jar/Berghofer12"}. This style of -operational semantics was originated by @{cite [cite_macro=citet] -"DBLP:journals/tcs/FelleisenH92"}. - -\ - -type_synonym ('answer, 'location, 'question, 'state) ctxt - = "('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com" - -inductive_set - ctxt :: "( ('answer, 'location, 'question, 'state) ctxt - \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com list) ) set" -where - C_Hole: "(id, \[]\) \ ctxt" -| C_Loop: "(E, fctxt) \ ctxt \ (\t. LOOP DO E t OD, \t. fctxt t @ [LOOP DO E t OD]) \ ctxt" -| C_Seq: "(E, fctxt) \ ctxt \ (\t. E t;; u, \t. fctxt t @ [u]) \ ctxt" -| C_Choose1: "(E, fctxt) \ ctxt \ (\t. E t \ u, fctxt) \ ctxt" -| C_Choose2: "(E, fctxt) \ ctxt \ (\t. u \ E t, fctxt) \ ctxt" - -inductive - basic_com :: "('answer, 'location, 'question, 'state) com \ bool" -where - "basic_com (\l\ Request action val)" -| "basic_com (\l\ Response action)" -| "basic_com (\l\ LocalOp R)" -| "basic_com (\l\ IF b THEN c FI)" -| "basic_com (\l\ IF b THEN c1 ELSE c2 FI)" -| "basic_com (\l\ WHILE b DO c OD)" -(*<*) - -declare basic_com.intros[intro!] basic_com.cases[elim] - -(*>*) -text\ +abbreviation cTKN :: "('answer, 'location, 'question, 'state) local_state \ 'location option" where + "cTKN s \ fst (snd s)" -We can decompose a small step into a context and a @{term -"basic_com"}. - -\ - -fun - decompose_com :: "('answer, 'location, 'question, 'state) com - \ ( ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'question, 'state) ctxt - \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com list) ) set" -where - "decompose_com (LOOP DO c1 OD) = { (c, \t. LOOP DO ictxt t OD, \t. fctxt t @ [LOOP DO ictxt t OD]) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 }" -| "decompose_com (c1;; c2) = { (c, \t. ictxt t;; c2, \t. fctxt t @ [c2]) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 }" -| "decompose_com (c1 \ c2) = { (c, \t. ictxt t \ c2, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 } - \ { (c, \t. c1 \ ictxt t, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c2 }" -| "decompose_com c = {(c, id, \[]\)}" - -definition - decomposeLS :: "('answer, 'location, 'question, 'state) local_state - \ ( ('answer, 'location, 'question, 'state) com - \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com) - \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com list) ) set" -where - "decomposeLS s \ case cPGM s of c # _ \ decompose_com c | _ \ {}" - -(*<*) -declare ctxt.intros[intro!] - -lemma ctxt_inj: - assumes "(E, fctxt) \ ctxt" - assumes "E x = E y" - shows "x = y" -using assms by (induct set: ctxt) auto - -lemma decompose_ctxt: - assumes "(c', ictxt, fctxt) \ decompose_com c" - shows "(ictxt, fctxt) \ ctxt" -using assms by (induct c arbitrary: c' ictxt fctxt) auto +abbreviation cLST :: "('answer, 'location, 'question, 'state) local_state \ 'state" where + "cLST s \ snd (snd s)" -lemma decompose_ictxt: - assumes "(c', ictxt, fctxt) \ decompose_com c" - shows "c = ictxt c'" -using assms by (induct c arbitrary: c' ictxt fctxt) auto -(*>*) -theorem context_decompose: - "s \\<^bsub>\\<^esub> s' \ (\(c, ictxt, fctxt) \ decomposeLS s. - cPGM s = ictxt c # tl (cPGM s) - \ basic_com c - \ (c # fctxt c @ tl (cPGM s), cLST s) \\<^bsub>\\<^esub> s')" -(*<*)(is "?lhs = ?rhs") -proof - assume ?lhs then show ?rhs - by (induct rule: small_step.induct) - (fastforce simp: decomposeLS_def)+ -next - have gen: "(c0 # cs, s) \\<^bsub>\\<^esub> s'" - if as: "(c # fctxt c @ cs, s) \\<^bsub>\\<^esub> s'" - and ds: "(c, ictxt, fctxt) \ decompose_com c0" - for cs c c0 ictxt fctxt l s s' - proof - - from ds have ic: "(ictxt, fctxt) \ ctxt" - unfolding decomposeLS_def by (auto intro: decompose_ctxt split: list.splits) - from ic as decompose_ictxt[OF ds] - show "(c0 # cs, s) \\<^bsub>\\<^esub> s'" - by (induct ictxt fctxt arbitrary: c0 cs set: ctxt) - (cases s', fastforce simp: fun_eq_iff dest: ctxt_inj)+ - qed - assume ?rhs then show ?lhs - by (cases s) - (auto simp: decomposeLS_def split: list.splits dest!: gen) -qed - -(*>*) -text\ - -While we only use this result left-to-right (to decompose a small step -into a basic one), this equivalence shows that we lose no information -in doing so. - -\ - -subsection\System steps\ +subsection\System steps \label{sec:cimp-system-steps}\ text\ -\label{sec:cimp-system-steps} - A global state maps process names to process' local states. One might hope to allow processes to have distinct types of local state, but there remains no good solution yet in a simply-typed setting; see @{cite [cite_macro=citet] "DBLP:journals/entcs/SchirmerW09"}. \ type_synonym ('answer, 'location, 'proc, 'question, 'state) global_state = "'proc \ ('answer, 'location, 'question, 'state) local_state" type_synonym ('proc, 'state) local_states = "'proc \ 'state" text\ An execution step of the overall system is either any enabled internal @{term "\"} step of any process, or a communication rendezvous between two processes. For the latter to occur, a @{const "Request"} action must be enabled in process @{term "p1"}, and a @{const "Response"} action in (distinct) process @{term "p2"}, where the request/response labels @{term "\"} and @{term "\"} (semantically) match. We also track global communication history here to support assertional -reasoning (see \S\ref{sec:cimp-assertions}). +reasoning (see \S\ref{sec:cimp-invariants}). \ type_synonym ('answer, 'question) event = "'question \ 'answer" type_synonym ('answer, 'question) history = "('answer, 'question) event list" -type_synonym ('answer, 'location, 'proc, 'question, 'state) system_state - = "('answer, 'location, 'proc, 'question, 'state) global_state - \ ('answer, 'question) history" - -inductive_set - system_step :: "( ('answer, 'ls, 'proc, 'question, 'state) system_state - \ ('answer, 'ls, 'proc, 'question, 'state) system_state ) set" -where - LocalStep: "\ s p \\<^bsub>\\<^esub> ls'; s' = s(p := ls'); h' = h \ \ ((s, h), (s', h')) \ system_step" -| CommunicationStep: "\ s p1 \\<^bsub>\\, \\\<^esub> ls1'; s p2 \\<^bsub>\\, \\\<^esub> ls2'; p1 \ p2; - s' = s(p1 := ls1', p2 := ls2'); h' = h @ [(\, \)] \ \ ((s, h), (s', h')) \ system_step" +record ('answer, 'location, 'proc, 'question, 'state) system_state = + GST :: "('answer, 'location, 'proc, 'question, 'state) global_state" + HST :: "('answer, 'question) history" -abbreviation - system_step_syn :: "('answer, 'ls, 'proc, 'question, 'state) system_state - \ ('answer, 'ls, 'proc, 'question, 'state) system_state \ bool" ("_ s\ _" [55, 56] 55) +inductive \\ This is a predicate of the current state, so the successor state comes first. \ + system_step :: "'proc set + \ ('answer, 'location, 'proc, 'question, 'state) system_state + \ ('answer, 'location, 'proc, 'question, 'state) system_state + \ bool" where - "sh s\ sh' \ (sh, sh') \ system_step" + LocalStep: "\ GST sh p \\<^bsub>\\<^esub> ls'; GST sh' = (GST sh)(p := ls'); HST sh' = HST sh \ \ system_step {p} sh' sh" +| CommunicationStep: "\ GST sh p \\<^bsub>\\, \\\<^esub> ls1'; GST sh q \\<^bsub>\\, \\\<^esub> ls2'; p \ q; + GST sh' = (GST sh)(p := ls1', q := ls2'); HST sh' = HST sh @ [(\, \)] \ \ system_step {p, q} sh' sh" -abbreviation - system_steps_syn :: "('answer, 'ls, 'proc, 'question, 'state) system_state - \ ('answer, 'ls, 'proc, 'question, 'state) system_state \ bool" ("_ s\\<^sup>* _" [55, 56] 55) -where - "sh s\\<^sup>* sh' \ (sh, sh') \ system_step\<^sup>*" -(*<*) - -(*>*) text\ In classical process algebras matching communication actions yield \\\ steps, which aids nested parallel composition and the restriction operation @{cite [cite_macro=citep] \\S2.2\ "Milner:1980"}. As CIMP does not provide either we do not need to hide communication labels. In CCS/CSP it is not clear how one reasons about the communication history, and it seems that assertional reasoning about these languages is not well developed. \ -subsection\Assertions\ +text\ + +We define predicates over communication histories and system states. These are uncurried to ease composition. + +\ + +type_synonym ('answer, 'location, 'proc, 'question, 'state) state_pred + = "('answer, 'location, 'proc, 'question, 'state) system_state \ bool" text\ -\label{sec:cimp-assertions} +The \LST\ operator (written as a postfix \\\) projects +the local states of the processes from a \<^typ>\('answer, 'location, 'proc, 'question, 'state) system_state\, i.e. it +discards control location information. -We now develop a technique for showing that a CIMP system satisfies a -single global invariant, following @{cite [cite_macro=citet] -"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"} -(and the later @{cite [cite_macro=citet] "DBLP:books/aw/Lamport2002"}) -and closely related work by @{cite [cite_macro=citet] -"AptFrancezDeRoever:1980"}, @{cite [cite_macro=citet] -"CousotCousot:1980"} and @{cite [cite_macro=citet] -"DBLP:journals/acta/LevinG81"}, which suggest the incorporation of a -history variable. @{cite [cite_macro=citet] "CousotCousot:1980"} -apparently contains a completeness proof. Lamport mentions that this -technique was well-known in the mid-80s when he proposed the use of -prophecy variables (see his webpage bibliography). See also @{cite -[cite_macro=citet] "DBLP:books/cu/RoeverBH2001"} for an extended -discussion of some of this. +Conversely the \LSTP\ operator lifts predicates over +local states into predicates over \<^typ>\('answer, 'location, 'proc, 'question, 'state) system_state\. -Achieving the right level of abstraction is a bit fiddly; we want to -avoid revealing too much of the program text as it -executes. Intuitively we wish to expose the processes's present -control locations and local states only. @{cite [cite_macro=citet] -"DBLP:journals/acta/Lamport80"} avoids these issues by only providing -an axiomatic semantics for his language. +Predicates that do not depend on control locations were termed @{emph +\universal assertions\} by @{cite [cite_macro=citet] +\\S3.6\ "DBLP:journals/acta/LevinG81"}. \ -subsubsection\Control predicates\ +type_synonym ('proc, 'state) local_state_pred + = "('proc, 'state) local_states \ bool" + +definition LST :: "('answer, 'location, 'proc, 'question, 'state) system_state + \ ('proc, 'state) local_states" ("_\" [1000] 1000) where + "s\ = cLST \ GST s" + +abbreviation (input) LSTP :: "('proc, 'state) local_state_pred + \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "LSTP P \ \s. P s\" + + +subsection\Control predicates \label{sec:cimp-control-predicates}\ text\ -\label{sec:cimp-control-predicates} - Following @{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80"}\footnote{@{cite [cite_macro=citet] "MannaPnueli:1995"} also develop a theory of locations. I think Lamport attributes control predicates to Owicki in her PhD thesis (under Gries). I did not find a treatment of procedures. @{cite -[cite_macro=citet] "MannaPnueli:1991"} observe that a set notation for -spreading assertions over sets of locations reduces clutter +[cite_macro=citet] "MannaPnueli:1991"} observe that a notation for +making assertions over sets of locations reduces clutter significantly.}, we define the \at\ predicate, which holds of a process when control resides at that location. Due to non-determinism processes can be \at\ a set of locations; it is more like ``a statement with this location is enabled'', which incidentally handles non-unique locations. Lamport's language is deterministic, so he doesn't have this problem. This also allows him to develop a stronger theory about his control predicates. \ +type_synonym 'location label = "'location set" + primrec - atC :: "('answer, 'location, 'question, 'state) com \ 'location \ bool" + atC :: "('answer, 'location, 'question, 'state) com \ 'location label" where - "atC (\l'\ Request action val) = (\l. l = l')" -| "atC (\l'\ Response action) = (\l. l = l')" -| "atC (\l'\ LocalOp f) = (\l. l = l')" -| "atC (\l'\ IF _ THEN _ FI) = (\l. l = l')" -| "atC (\l'\ IF _ THEN _ ELSE _ FI) = (\l. l = l')" -| "atC (\l'\ WHILE _ DO _ OD) = (\l. l = l')" + "atC (\l\ Request action val) = {l}" +| "atC (\l\ Response action) = {l}" +| "atC (\l\ LocalOp f) = {l}" +| "atC (\l\ IF _ THEN _ FI) = {l}" +| "atC (\l\ IF _ THEN _ ELSE _ FI) = {l}" +| "atC (\l\ WHILE _ DO _ OD) = {l}" | "atC (LOOP DO c OD) = atC c" | "atC (c1;; c2) = atC c1" -| "atC (c1 \ c2) = (atC c1 \<^bold>\ atC c2)" - -primrec atL :: "('answer, 'location, 'question, 'state) com list \ 'location \ bool" where - "atL [] = \False\" -| "atL (c # _) = atC c" - -abbreviation atLS :: "('answer, 'location, 'question, 'state) local_state \ 'location \ bool" where - "atLS \ \s. atL (cPGM s)" -(*<*) - -lemma at_decompose: - "(c, ictxt, fctxt) \ decompose_com c0 \ (\l. atC c l \ atC c0 l)" -by (induct c0 arbitrary: c ictxt fctxt) fastforce+ - -lemma at_decomposeLS: - "(c, ictxt, fctxt) \ decomposeLS s \ (\l. atC c l \ atLS s l)" -by (auto simp: decomposeLS_def at_decompose split: list.splits) - -(*>*) -text\ +| "atC (c1 \ c2) = atC c1 \ atC c2" -We define predicates over communication histories and a projection of -global states. These are uncurried to ease composition. - -\ - -type_synonym ('location, 'proc, 'state) pred_local_state - = "'proc \ (('location \ bool) \ 'state)" - -record ('answer, 'location, 'proc, 'question, 'state) pred_state = - local_states :: "('location, 'proc, 'state) pred_local_state" - hist :: "('answer, 'question) history" +primrec atCs :: "('answer, 'location, 'question, 'state) com list \ 'location label" where + "atCs [] = {}" +| "atCs (c # _) = atC c" -type_synonym ('answer, 'location, 'proc, 'question, 'state) pred - = "('answer, 'location, 'proc, 'question, 'state) pred_state \ bool" - -definition mkP :: "('answer, 'location, 'proc, 'question, 'state) system_state \ ('answer, 'location, 'proc, 'question, 'state) pred_state" where - "mkP \ \(s, h). \ local_states = \p. case s p of (cs, ps) \ (atL cs, ps), hist = h \" -(*<*) - -lemma hist_mkP[iff]: - "hist (mkP (s, h)) = h" -by (simp add: mkP_def) - -(*>*) text\ We provide the following definitions to the end-user. \AT\ maps process names to a predicate that is true of -locations where control for that process resides. The abbreviation -\at\ shuffles its parameters; the former is -simplifier-friendly and eta-reduced, while the latter is convenient -for writing assertions. - -\ - -definition AT :: "('answer, 'location, 'proc, 'question, 'state) pred_state \ 'proc \ 'location \ bool" where - "AT \ \s p l. fst (local_states s p) l" - -abbreviation at :: "'proc \ 'location \ ('answer, 'location, 'proc, 'question, 'state) pred" where - "at p l s \ AT s p l" - -text\ - -Often we wish to talk about control residing at one of a set of -locations. This stands in for, and generalises, the \in\ -predicate of @{cite [cite_macro=citet] +locations where control for that process resides, and the abbreviation \at\ provides a conventional +way to use it. The constant \atS\ specifies that control for process \p\ resides at one of +the given locations. This stands in for, and generalises, the \in\ predicate of @{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80"}. \ -definition atS :: "'proc \ 'location set \ ('answer, 'location, 'proc, 'question, 'state) pred" where - "atS \ \p ls s. \l\ls. at p l s" +definition AT :: "('answer, 'location, 'proc, 'question, 'state) system_state \ 'proc \ 'location label" where + "AT s p = atCs (cPGM (GST s p))" + +abbreviation at :: "'proc \ 'location \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "at p l s \ l \ AT s p" + +definition atS :: "'proc \ 'location set \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "atS p ls s = (\l\ls. at p l s)" + +(* FIXME rename, document, rules. Identifies a process's control state label precisely as one element of a set. *) +definition atLs :: "'proc \ 'location label set \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "atLs p labels s = (AT s p \ labels)" + +(* FIXME rename, document. Identifies a process's control state label precisely. Relate atL to at/atS, ex/ *) +abbreviation (input) atL :: "'proc \ 'location label \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "atL p label \ atLs p {label}" + +(* FIXME rename, document. Processes are at the given labels. *) +definition atPLs :: "('proc \ 'location label) set \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "atPLs pls = (\<^bold>\p label. \(p, label) \ pls\ \<^bold>\ atL p label)" text\ +The constant \taken\ provides a way of identifying which transition was taken. It is somewhat like +Lamport's \after\, but not quite due to the presence of non-determinism here. This does not work well +for invariants or preconditions. + +\ + +definition taken :: "'proc \ 'location \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "taken p l s \ cTKN (GST s p) = Some l" + +text\ + +\label{sec:cimp-termination} + A process is terminated if it not at any control location. \ -abbreviation terminated :: "'proc \ ('answer, 'location, 'proc, 'question, 'state) pred" where - "terminated p s \ \l. \at p l s" - -text\ - -The \LST\ operator (written as a postfix \\\) projects -the local states of the processes from a \pred_state\, i.e. it -discards control location information. - -Conversely the \LSTP\ operator lifts predicates over -local states into predicates over \pred_state\. @{cite -[cite_macro=citet] \\S3.6\ "DBLP:journals/acta/LevinG81"} -call such predicates \emph{universal assertions}. - -\ - -type_synonym ('proc, 'state) state_pred - = "('proc, 'state) local_states \ bool" - -definition LST :: "('answer, 'location, 'proc, 'question, 'state) pred_state - \ ('proc, 'state) local_states" ("_\" [1000] 1000) where - "s\ \ snd \ local_states s" - -abbreviation (input) LSTP :: "('proc, 'state) state_pred - \ ('answer, 'location, 'proc, 'question, 'state) pred" where - "LSTP P \ \s. P (LST s)" +abbreviation (input) terminated :: "'proc \ ('answer, 'location, 'proc, 'question, 'state) state_pred" where + "terminated p \ atL p {}" text\ -By default we ask the simplifier to rewrite @{const "atS"} using -ambient @{const "AT"} information. - -\ - -lemma atS_state_cong[cong]: - "\ AT s p = AT s' p \ \ atS p ls s \ atS p ls s'" -by (auto simp: atS_def) - -text\ - -We provide an incomplete set of basic rules for label sets. - -\ - -lemma atS_simps: - "\atS p {} s" - "atS p {l} s \ at p l s" - "\ at p l s; l \ ls \ \ atS p ls s \ True" - "(\l. at p l s \ l \ ls) \ atS p ls s \ False" -by (auto simp: atS_def) - -lemma atS_mono: - "\ atS p ls s; ls \ ls' \ \ atS p ls' s" -by (auto simp: atS_def) - -lemma atS_un: - "atS p (l \ l') s \ atS p l s \ atS p l' s" -by (auto simp: atS_def) - -subsubsection\Invariants\ - -text\ - -\label{sec:cimp-invariants} - A complete system consists of one program per process, and a (global) constraint on their initial local states. From these we can construct the set of initial global states and all those reachable by system steps (\S\ref{sec:cimp-system-steps}). \ type_synonym ('answer, 'location, 'proc, 'question, 'state) programs = "'proc \ ('answer, 'location, 'question, 'state) com" -type_synonym ('answer, 'location, 'proc, 'question, 'state) system - = "('answer, 'location, 'proc, 'question, 'state) programs - \ ('proc, 'state) state_pred" +record ('answer, 'location, 'proc, 'question, 'state) pre_system = + PGMs :: "('answer, 'location, 'proc, 'question, 'state) programs" + INIT :: "('proc, 'state) local_state_pred" definition - initial_states :: "('answer, 'location, 'proc, 'question, 'state) system - \ ('answer, 'location, 'proc, 'question, 'state) global_state set" + initial_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext + \ ('answer, 'location, 'proc, 'question, 'state) global_state + \ bool" where - "initial_states sys \ - { f . (\p. cPGM (f p) = [fst sys p]) \ snd sys (cLST \ f) }" - -definition - reachable_states :: "('answer, 'location, 'proc, 'question, 'state) system - \ ('answer, 'location, 'proc, 'question, 'state) system_state set" -where - "reachable_states sys \ system_step\<^sup>* `` (initial_states sys \ {[]})" + "initial_state sys s = ((\p. cPGM (s p) = [PGMs sys p] \ cTKN (s p) = None) \ INIT sys (cLST \ s))" text\ -The following is a slightly more convenient induction rule for the set -of reachable states. - -\ - -lemma reachable_states_system_step_induct[consumes 1, - case_names init LocalStep CommunicationStep]: - assumes r: "(s, h) \ reachable_states sys" - assumes i: "\s. s \ initial_states sys \ P s []" - assumes l: "\s h ls' p. \ (s, h) \ reachable_states sys; P s h; s p \\<^bsub>\\<^esub> ls' \ - \ P (s(p := ls')) h" - assumes c: "\s h ls1' ls2' p1 p2 \ \. - \ (s, h) \ reachable_states sys; P s h; - s p1 \\<^bsub>\\, \\\<^esub> ls1'; s p2 \\<^bsub>\\, \\\<^esub> ls2'; p1 \ p2 \ - \ P (s(p1 := ls1', p2 := ls2')) (h @ [(\, \)])" - shows "P s h" -(*<*) -proof - - have "P s' h'" if "(s, []) s\\<^sup>* (s', h')" "s \ initial_states sys" for s s' h' - using that - by (induct rule: rtrancl_induct2) - (fastforce simp: reachable_states_def elim: system_step.cases intro: i l c)+ - with r show ?thesis by (clarsimp simp: reachable_states_def) -qed +We construct infinite runs of a system by allowing stuttering, i.e., arbitrary repetitions of states +following @{cite [cite_macro=citet] \Chapter~8\"Lamport:2002"}, by taking the reflexive +closure of the @{const system_step} relation. Therefore terminated +programs infinitely repeat their final state (but note our definition +of terminated processes in \S\ref{sec:cimp-termination}). -lemma initial_statesD: - "s \ initial_states sys \ AT (mkP (s, [])) = atC \ fst sys \ snd sys (mkP (s, []))\" -by (simp add: initial_states_def mkP_def split_def o_def LST_def AT_def) - -lemma initial_states_mkP[iff]: - "s \ initial_states sys \ at p l (mkP (s, [])) \ atC (fst sys p) l" -by (simp add: initial_states_def mkP_def split_def AT_def) - -(*>*) -subsubsection\Relating reachable states to the initial programs\ - -text\ - -\label{sec:cimp-decompose-small-step} - -To usefully reason about the control locations presumably embedded in -the single global invariant, we need to link the programs we have in -reachable state \s\ to the programs in the initial states. The -\fragments\ function decomposes the program into statements -that can be directly executed (\S\ref{sec:cimp-decompose}). We also -compute the locations we could be at after executing that statement as -a function of the process's local state. - -We could support Lamport's \after\ control predicate with more -syntactic analysis of this kind. +Some accounts define stuttering as the @{emph \finite\} repetition of states. With or without this constraint +\prerun\ contains @{emph \junk\} in the form of unfair runs, where particular processes do not progress. \ -fun - extract_cond :: "('answer, 'location, 'question, 'state) com \ 'state bexp" -where - "extract_cond (\l\ IF b THEN c FI) = b" -| "extract_cond (\l\ IF b THEN c1 ELSE c2 FI) = b" -| "extract_cond (\l\ WHILE b DO c OD) = b" -| "extract_cond c = \False\" - -type_synonym ('answer, 'location, 'question, 'state) loc_comp - = "('answer, 'location, 'question, 'state) com - \ 'state \ 'location \ bool" - -fun lconst :: "('location \ bool) \ ('answer, 'location, 'question, 'state) loc_comp" where - "lconst lp b s = lp" - -definition lcond :: "('location \ bool) \ ('location \ bool) - \ ('answer, 'location, 'question, 'state) loc_comp" where - "lcond lp lp' c s \ if extract_cond c s then lp else lp'" -(*<*) - -lemma lcond_split: - "Q (lcond lp lp' c s) \ (extract_cond c s \ Q lp) \ (\extract_cond c s \ Q lp')" -by (simp add: lcond_def split: if_splits) - -lemma lcond_split_asm: - "Q (lcond lp lp' c s) \ \ ((extract_cond c s \ \Q lp) \ (\extract_cond c s \ \ Q lp'))" -by (simp add: lcond_def split: if_splits) - -lemmas lcond_splits = lcond_split lcond_split_asm -(*>*) - -fun - fragments :: "('answer, 'location, 'question, 'state) com - \ ('location \ bool) - \ ( ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'question, 'state) loc_comp ) set" +definition + system_step_reflclp :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred" where - "fragments (\l\ IF b THEN c FI) ls - = { (\l\ IF b THEN c' FI, lcond (atC c) ls) |c'. True } - \ fragments c ls" -| "fragments (\l\ IF b THEN c1 ELSE c2 FI) ls - = { (\l\ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2)) |c1' c2'. True } - \ fragments c1 ls \ fragments c2 ls" -| "fragments (LOOP DO c OD) ls = fragments c (atC c)" -| "fragments (\l'\ WHILE b DO c OD) ls - = { (\l'\ WHILE b DO c' OD, lcond (atC c) ls) |c'. True } \ fragments c (\l. l = l')" -| "fragments (c1;; c2) ls = fragments c1 (atC c2) \ fragments c2 ls" -| "fragments (c1 \ c2) ls = fragments c1 ls \ fragments c2 ls" -| "fragments c ls = { (c, lconst ls) }" + "system_step_reflclp \ \ (\sh sh'. \pls. system_step pls sh' sh)\<^sup>=\<^sup>= (\ 0) (\ 1)" -fun - fragmentsL :: "('answer, 'location, 'question, 'state) com list - \ ( ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'question, 'state) loc_comp ) set" +definition + prerun :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext + \ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred" where - "fragmentsL [] = {}" -| "fragmentsL [c] = fragments c \False\" -| "fragmentsL (c # c' # cs) = fragments c (atC c') \ fragmentsL (c' # cs)" - -abbreviation - fragmentsLS :: "('answer, 'location, 'question, 'state) local_state - \ ( ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'question, 'state) loc_comp ) set" -where - "fragmentsLS s \ fragmentsL (cPGM s)" -(*<*) + "prerun sys = ((\\. initial_state sys (GST (\ 0)) \ HST (\ 0) = []) \<^bold>\ \system_step_reflclp)" -lemma fragmentsL_mono_Cons[iff]: - "fragmentsL cs \ fragmentsL (c # cs)" -by (induct cs) auto +definition \\ state-based invariants only \ + prerun_valid :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext + \ ('answer, 'location, 'proc, 'question, 'state) state_pred \ bool" ("_ \\<^bsub>pre\<^esub> _" [11, 0] 11) (* FIXME priorities *) +where + "(sys \\<^bsub>pre\<^esub> \) \ (\\. prerun sys \ \ (\\\\) \)" -lemma small_step_fragmentsLS: - assumes "s \\<^bsub>\\<^esub> s'" - shows "fragmentsLS s' \ fragmentsLS s" -using assms by (induct rule: small_step.induct) (case_tac [!] cs, auto) - -lemmas small_step_fragmentsLS_mem = subsetD[OF small_step_fragmentsLS] - -(*>*) text\ -Eliding the bodies of \IF\ and \WHILE\ statements -yields smaller (but equivalent) proof obligations. - -We show that taking system steps preserves fragments. +A \run\ of a system is a @{const \prerun\} that satisfies the \FAIR\ requirement. +Typically this would include @{emph \weak fairness\} for every transition of every process. \ -lemma reachable_states_fragmentsLS: - assumes "(s, h) \ reachable_states sys" - shows "fragmentsLS (s p) \ fragments (fst sys p) \False\" -(*<*) -using assms -by (induct rule: reachable_states_system_step_induct) - (auto simp: initial_states_def dest: small_step_fragmentsLS_mem) -(*>*) - -text\ - -Decomposing a compound command preserves fragments too. - -\ - -fun - extract_inner_locations :: "('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'question, 'state) com list - \ ('answer, 'location, 'question, 'state) loc_comp" -where - "extract_inner_locations (\l\ IF b THEN c FI) cs = lcond (atC c) (atL cs)" -| "extract_inner_locations (\l\ IF b THEN c1 ELSE c2 FI) cs = lcond (atC c1) (atC c2)" -| "extract_inner_locations (LOOP DO c OD) cs = lconst (atC c)" -| "extract_inner_locations (\l\ WHILE b DO c OD) cs = lcond (atC c) (atL cs)" -| "extract_inner_locations c cs = lconst (atL cs)" - -(*<*) - -lemma decompose_fragments: - assumes "(c, ictxt, fctxt) \ decompose_com c0" - shows "(c, extract_inner_locations c (fctxt c @ cs)) \ fragments c0 (atL cs)" -using assms -proof(induct c0 arbitrary: c ictxt fctxt cs) - case (Loop c01 c ictxt fctxt cs) - from Loop.prems Loop.hyps(1)[where cs="ictxt c # cs"] show ?case by (auto simp: decompose_ictxt[symmetric]) -next - case (Seq c01 c02 c ictxt fctxt cs) - from Seq.prems Seq.hyps(1)[where cs="c02 # cs"] show ?case by auto -qed auto +record ('answer, 'location, 'proc, 'question, 'state) system = + "('answer, 'location, 'proc, 'question, 'state) pre_system" ++ FAIR :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred" -lemma decomposeLS_fragmentsLS: - assumes "(c, ictxt, fctxt) \ decomposeLS s" - shows "(c, extract_inner_locations c (fctxt c @ tl (cPGM s))) \ fragmentsLS s" -using assms -proof(cases "cPGM s") - case (Cons d ds) - with assms decompose_fragments[where cs="ds"] - show ?thesis by (cases ds) (auto simp: decomposeLS_def) -qed (simp add: decomposeLS_def) -(*>*) - -lemma small_step_extract_inner_locations: - assumes "basic_com c" - assumes "(c # cs, ls) \\<^bsub>\\<^esub> ls'" - shows "extract_inner_locations c cs c ls = atLS ls'" -using assms by (fastforce split: lcond_splits) - -text\ - -The headline result allows us to constrain the initial and final states -of a given small step in terms of the original programs, provided the -initial state is reachable. - -\ +definition + run :: "('answer, 'location, 'proc, 'question, 'state) system + \ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred" +where + "run sys = (prerun sys \<^bold>\ FAIR sys)" -theorem decompose_small_step: - assumes "s p \\<^bsub>\\<^esub> ps'" - assumes "(s, h) \ reachable_states sys" - obtains c cs ls' - where "(c, ls') \ fragments (fst sys p) \False\" - and "basic_com c" - and "\l. atC c l \ atLS (s p) l" - and "ls' c (cLST (s p)) = atLS ps'" - and "(c # cs, cLST (s p)) \\<^bsub>\\<^esub> ps'" -(*<*) -using assms -apply - -apply (frule iffD1[OF context_decompose]) -apply clarsimp -apply (frule decomposeLS_fragmentsLS) -apply (frule at_decomposeLS) -apply (frule (1) subsetD[OF reachable_states_fragmentsLS, rotated]) -apply (frule (1) small_step_extract_inner_locations[rotated]) -apply auto -done - -(*>*) -text\ - -Reasoning with @{thm [source] "reachable_states_system_step_induct"} -and @{thm [source] "decompose_small_step"} is quite tedious. We -provide a very simple VCG that generates friendlier local proof -obligations. - -\ +definition + valid :: "('answer, 'location, 'proc, 'question, 'state) system + \ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred \ bool" ("_ \ _" [11, 0] 11) (* FIXME priorities *) +where + "(sys \ \) \ (\\. run sys \ \ \ \)" (*<*) end (*>*) diff --git a/thys/ConcurrentIMP/CIMP_one_place_buffer_ex.thy b/thys/ConcurrentIMP/CIMP_one_place_buffer_ex.thy deleted file mode 100644 --- a/thys/ConcurrentIMP/CIMP_one_place_buffer_ex.thy +++ /dev/null @@ -1,192 +0,0 @@ -(*<*) -(* - * Copyright 2015, NICTA - * - * This software may be distributed and modified according to the terms of - * the BSD 2-Clause license. Note that NO WARRANTY is provided. - * See "LICENSE_BSD2.txt" for details. - * - * @TAG(NICTA_BSD) - *) - -theory CIMP_one_place_buffer_ex -imports - CIMP -begin - -(*>*) -section\One-place buffer example\ - -text\ - -\label{sec:one_place_buffer} - -To demonstrate the CIMP reasoning infrastructure, we treat the trivial -one-place buffer example of @{cite [cite_macro=citet] -\\S3.3\ "DBLP:journals/toplas/LamportS84"}. Note that the -semantics for our language is different to @{cite -[cite_macro=citeauthor] "DBLP:journals/toplas/LamportS84"}'s, who -treated a historical variant of CSP (i.e., not the one in @{cite -"Hoare:1985"}). - -We introduce some syntax for fixed-topology (static channel-based) -scenarios. - -\ - -abbreviation - Receive :: "'location \ 'channel \ ('val \ 'state \ 'state) - \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_") -where - "\l\ ch\f \ \l\ Response (\quest s. if fst quest = ch then {(f (snd quest) s, ())} else {})" - -abbreviation - Send :: "'location \ 'channel \ ('state \ 'val) - \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_") -where - "\l\ ch\f \ \l\ Request (\s. (ch, f s)) (\ans s. {s})" - -text\ - -We further specialise these for our particular example. - -\ - -abbreviation - Receive' :: "'location \ 'channel \ (unit, 'location, 'channel \ 'state, 'state) com" ("\_\/ _\") -where - "\l\ ch\ \ \l\ ch\(\v _. v)" - -abbreviation - Send' :: "'location \ 'channel \ (unit, 'location, 'channel \ 'state, 'state) com" ("\_\/ _\") -where - "\l\ ch\ \ \l\ ch\id" - -text\ - -These definitions largely follow @{cite [cite_macro=citet] -"DBLP:journals/toplas/LamportS84"}. We have three processes -communicating over two channels. We enumerate program locations. - -\ - -datatype ex_chname = \12 | \23 -type_synonym ex_val = nat -type_synonym ex_ch = "ex_chname \ ex_val" -datatype ex_loc = r12 | r23 | s23 | s12 -datatype ex_proc = p1 | p2 | p3 - -type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_val) com" -type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_val) pred" -type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_val) global_state" -type_synonym ex_system = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system" -type_synonym ex_history = "(ex_ch \ unit) list" - -primrec - ex_pgms :: "ex_proc \ ex_pgm" -where - "ex_pgms p1 = \s12\ \12\" -| "ex_pgms p2 = LOOP DO \r12\ \12\;; \s23\ \23\ OD" -| "ex_pgms p3 = \r23\ \23\" - -text\ - -Each process starts with an arbitrary initial local state. - -\ - -abbreviation ex_init :: "(ex_proc \ ex_val) \ bool" where - "ex_init \ \True\" - -abbreviation ex_system :: "ex_system" where - "ex_system \ (ex_pgms, ex_init)" - -text\ - -The following adapts Kai Engelhardt's, from his notes titled -\emph{Proving an Asynchronous Message Passing Program Correct}, -2011. The history variable tracks the causality of the system, which I -feel is missing in Lamport's treatment. We tack on Lamport's invariant -so we can establish \Etern_pred\. - -\ - -abbreviation - filter_on_channel :: "ex_chname \ ex_history \ ex_val list" -where - "filter_on_channel ch \ map (snd \ fst) \ filter ((=) ch \ fst \ fst)" - -definition Ip1_0 :: ex_pred where - "Ip1_0 \ at p1 s12 \<^bold>\ (\s. filter_on_channel \12 (hist s) = [])" -definition Ip1_1 :: ex_pred where - "Ip1_1 \ terminated p1 \<^bold>\ (\s. filter_on_channel \12 (hist s) = [LST s p1])" - -definition Ip2_0 :: ex_pred where - "Ip2_0 \ at p2 r12 \<^bold>\ (\s. filter_on_channel \12 (hist s) = filter_on_channel \23 (hist s))" -definition Ip2_1 :: ex_pred where - "Ip2_1 \ at p2 s23 \<^bold>\ (\s. filter_on_channel \12 (hist s) = filter_on_channel \23 (hist s) @ [LST s p2] - \ LST s p1 = LST s p2)" - -definition Ip3_0 :: ex_pred where - "Ip3_0 \ at p3 r23 \<^bold>\ (\s. filter_on_channel \23 (hist s) = [])" -definition Ip3_1 :: ex_pred where - "Ip3_1 \ terminated p3 \<^bold>\ (\s. filter_on_channel \23 (hist s) = [LST s p2] - \ LST s p1 = LST s p3)" - -definition I_pred :: ex_pred where - "I_pred \ pred_conjoin [ Ip1_0, Ip1_1, Ip2_0, Ip2_1, Ip3_0, Ip3_1 ]" - -lemmas I_defs = Ip1_0_def Ip1_1_def Ip2_0_def Ip2_1_def Ip3_0_def Ip3_1_def - -text\ - -If process three terminates, then it has process one's value. This is -stronger than @{cite [cite_macro=citeauthor] -"DBLP:journals/toplas/LamportS84"}'s as we don't ask that the first -process has also terminated. - -\ - -definition Etern_pred :: ex_pred where - "Etern_pred \ terminated p3 \<^bold>\ (\s. LST s p1 = LST s p3)" - -text\ - -Proofs from here down. - -\ - -lemma correct_system: - "I_pred sh \ Etern_pred sh" -apply (clarsimp simp: Etern_pred_def I_pred_def I_defs) -done - -lemma p1: "ex_pgms, p1, lconst \False\ \ \I_pred\ \s12\ \12\\s. s" -apply (rule vcg.intros) -apply (rename_tac p') -apply (case_tac p') - apply (auto simp: I_pred_def I_defs atS_def) -done - -lemma p2_1: "ex_pgms, p2, lconst (\l. l = r12) \ \I_pred\ \s23\ \23\\s. s" -apply (rule vcg.intros) -apply (rename_tac p') -apply (case_tac p') - apply (auto simp: I_pred_def I_defs atS_def) -done - -lemma "(s, h) \ reachable_states ex_system \ I_pred (mkP (s, h))" -apply (erule VCG) - apply (clarsimp simp: I_pred_def I_defs atS_def) -apply simp -apply (rename_tac p) -apply (case_tac p) - apply auto (* vcg_clarsimp_tac *) - apply (auto simp: p1 p2_1) -done - -text\\ -(*<*) - -end -(*>*) diff --git a/thys/ConcurrentIMP/CIMP_pred.thy b/thys/ConcurrentIMP/CIMP_pred.thy --- a/thys/ConcurrentIMP/CIMP_pred.thy +++ b/thys/ConcurrentIMP/CIMP_pred.thy @@ -1,138 +1,169 @@ (*<*) (* * Copyright 2015, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) theory CIMP_pred imports Main begin +(* Extra HOL *) + +lemma triv: "P \ P" +by simp + +lemma always_eventually_pigeonhole: + "(\i. \n\i. \m\k. P m n) \ (\m\k::nat. \i::nat. \n\i. P m n)" +proof(induct k) + case (Suc k) then show ?case + apply (auto 8 0) + using le_SucI apply blast + apply (metis (full_types) le_Suc_eq nat_le_linear order_trans) + done +qed simp + (*>*) section\ Point-free notation \ text\ \label{sec:cimp-lifted-predicates} Typically we define predicates as functions of a state. The following provide a somewhat comfortable point-free imitation of Isabelle/HOL's operators. \ abbreviation (input) pred_K :: "'b \ 'a \ 'b" ("\_\") where "\f\ \ \s. f" abbreviation (input) - pred_not :: "('a \ bool) \ 'a \ bool" ("\<^bold>\") where + pred_not :: "('a \ bool) \ 'a \ bool" ("\<^bold>\ _" [40] 40) where "\<^bold>\a \ \s. \a s" abbreviation (input) pred_conj :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" (infixr "\<^bold>\" 35) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) pred_disj :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" (infixr "\<^bold>\" 30) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) pred_implies :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" (infixr "\<^bold>\" 25) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) + pred_iff :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" (infixr "\<^bold>\" 25) where + "a \<^bold>\ b \ \s. a s \ b s" + +abbreviation (input) pred_eq :: "('a \ 'b) \ ('a \ 'b) \ 'a \ bool" (infix "\<^bold>=" 40) where "a \<^bold>= b \ \s. a s = b s" abbreviation (input) pred_member :: "('a \ 'b) \ ('a \ 'b set) \ 'a \ bool" (infix "\<^bold>\" 40) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) pred_neq :: "('a \ 'b) \ ('a \ 'b) \ 'a \ bool" (infix "\<^bold>\" 40) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) pred_If :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'b) \ 'a \ 'b" ("(If (_)/ Then (_)/ Else (_))" [0, 0, 10] 10) where "If P Then x Else y \ \s. if P s then x s else y s" abbreviation (input) pred_less :: "('a \ 'b::ord) \ ('a \ 'b) \ 'a \ bool" (infix "\<^bold><" 40) where "a \<^bold>< b \ \s. a s < b s" abbreviation (input) pred_le :: "('a \ 'b::ord) \ ('a \ 'b) \ 'a \ bool" (infix "\<^bold>\" 40) where "a \<^bold>\ b \ \s. a s \ b s" abbreviation (input) pred_plus :: "('a \ 'b::plus) \ ('a \ 'b) \ 'a \ 'b" (infixl "\<^bold>+" 65) where "a \<^bold>+ b \ \s. a s + b s" abbreviation (input) pred_minus :: "('a \ 'b::minus) \ ('a \ 'b) \ 'a \ 'b" (infixl "\<^bold>-" 65) where "a \<^bold>- b \ \s. a s - b s" abbreviation (input) fun_fanout :: "('a \ 'b) \ ('a \ 'c) \ 'a \ 'b \ 'c" (infix "\<^bold>\" 35) where "f \<^bold>\ g \ \x. (f x, g x)" abbreviation (input) pred_all :: "('b \ 'a \ bool) \ 'a \ bool" (binder "\<^bold>\" 10) where "\<^bold>\x. P x \ \s. \x. P x s" abbreviation (input) pred_ex :: "('b \ 'a \ bool) \ 'a \ bool" (binder "\<^bold>\" 10) where "\<^bold>\x. P x \ \s. \x. P x s" abbreviation (input) pred_app :: "('b \ 'a \ 'c) \ ('a \ 'b) \ 'a \ 'c" (infixl "\<^bold>$" 100) where "f \<^bold>$ g \ \s. f (g s) s" abbreviation (input) pred_subseteq :: "('a \ 'b set) \ ('a \ 'b set) \ 'a \ bool" (infix "\<^bold>\" 50) where "A \<^bold>\ B \ \s. A s \ B s" abbreviation (input) pred_union :: "('a \ 'b set) \ ('a \ 'b set) \ 'a \ 'b set" (infixl "\<^bold>\" 65) where "a \<^bold>\ b \ \s. a s \ b s" +abbreviation (input) + pred_inter :: "('a \ 'b set) \ ('a \ 'b set) \ 'a \ 'b set" (infixl "\<^bold>\" 65) where + "a \<^bold>\ b \ \s. a s \ b s" + text\ More application specific. \ abbreviation (input) pred_conjoin :: "('a \ bool) list \ 'a \ bool" where "pred_conjoin xs \ foldr (\<^bold>\) xs \True\" abbreviation (input) + pred_disjoin :: "('a \ bool) list \ 'a \ bool" where + "pred_disjoin xs \ foldr (\<^bold>\) xs \False\" + +abbreviation (input) pred_is_none :: "('a \ 'b option) \ 'a \ bool" ("NULL _" [40] 40) where "NULL a \ \s. a s = None" abbreviation (input) pred_empty :: "('a \ 'b set) \ 'a \ bool" ("EMPTY _" [40] 40) where "EMPTY a \ \s. a s = {}" abbreviation (input) pred_list_null :: "('a \ 'b list) \ 'a \ bool" ("LIST'_NULL _" [40] 40) where "LIST_NULL a \ \s. a s = []" abbreviation (input) + pred_list_append :: "('a \ 'b list) \ ('a \ 'b list) \ 'a \ 'b list" (infixr "\<^bold>@" 65) where + "xs \<^bold>@ ys \ \s. xs s @ ys s" + +abbreviation (input) pred_pair :: "('a \ 'b) \ ('a \ 'c) \ 'a \ 'b \ 'c" (infixr "\<^bold>\" 60) where "a \<^bold>\ b \ \s. (a s, b s)" abbreviation (input) pred_singleton :: "('a \ 'b) \ 'a \ 'b set" where "pred_singleton x \ \s. {x s}" (*<*) end (*>*) diff --git a/thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy b/thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy deleted file mode 100644 --- a/thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy +++ /dev/null @@ -1,168 +0,0 @@ -(*<*) -(* - * Copyright 2015, NICTA - * - * This software may be distributed and modified according to the terms of - * the BSD 2-Clause license. Note that NO WARRANTY is provided. - * See "LICENSE_BSD2.txt" for details. - * - * @TAG(NICTA_BSD) - *) - -theory CIMP_unbounded_buffer_ex -imports - CIMP - "HOL-Library.Prefix_Order" -begin - -abbreviation - Receive :: "'location \ 'channel \ ('val \ 'state \ 'state) - \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_") -where - "\l\ ch\f \ \l\ Response (\quest s. if fst quest = ch then {(f (snd quest) s, ())} else {})" - -abbreviation - Send :: "'location \ 'channel \ ('state \ 'val) - \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_") -where - "\l\ ch\f \ \l\ Request (\s. (ch, f s)) (\ans s. {s})" - -lemma butlastE: - "\ butlast xs = ys; xs \ []; \z. xs = ys @ [z] \ P \ \ P" -by (induct xs rule: rev_induct) auto - -(*>*) -section\Unbounded buffer example\ - -text\ - -\label{sec:unbounded_place_buffer} - -This is more literally Kai's example from his notes titled -\emph{Proving an Asynchronous Message Passing Program Correct}, 2011. - -\ - -datatype ex_chname = \12 | \23 -type_synonym ex_val = nat -type_synonym ex_ls = "ex_val list" -type_synonym ex_ch = "ex_chname \ ex_val" -datatype ex_loc = \4 | \5 | c1 | r12 | r23 | s23 | s12 -datatype ex_proc = p1 | p2 | p3 - -type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_ls) com" -type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) pred" -type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) global_state" -type_synonym ex_system = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) system" -type_synonym ex_history = "(ex_ch \ unit) list" - -text\ - -FIXME a bit fake: the local state for the producer process contains -all values produced. - -\ - -primrec ex_pgms :: "ex_proc \ ex_pgm" where - "ex_pgms p1 = LOOP DO \c1\ LocalOp (\xs. { xs @ [x] |x. True }) ;; \s12\ \12\last OD" -| "ex_pgms p2 = LOOP DO \r12\ \12\(\x xs. xs @ [x]) - \ \\4\ IF (\s. length s > 0) THEN \s23\ Request (\s. (\23, hd s)) (\ans s. {tl s}) FI - OD" -| "ex_pgms p3 = LOOP DO \r23\ \23\(\x xs. xs @ [x]) OD" - -abbreviation ex_init :: "(ex_proc \ ex_ls) \ bool" where - "ex_init f \ \p. f p = []" - -abbreviation ex_system :: "ex_system" where - "ex_system \ (ex_pgms, ex_init)" - -definition filter_on_channel :: "ex_chname \ ex_history \ ex_val list" where - "filter_on_channel ch \ map (snd \ fst) \ filter ((=) ch \ fst \ fst)" - -lemma filter_on_channel_simps [simp]: - "filter_on_channel ch [] = []" - "filter_on_channel ch (xs @ ys) = filter_on_channel ch xs @ filter_on_channel ch ys" - "filter_on_channel ch (((ch', v), resp) # vals) = (if ch' = ch then [v] else []) @ filter_on_channel ch vals" -by (simp_all add: filter_on_channel_def) - -definition Ip1_0 :: ex_pred where - "Ip1_0 \ \s. at p1 c1 s \ filter_on_channel \12 (hist s) = s\ p1" -definition Ip1_1 :: ex_pred where - "Ip1_1 \ \s. at p1 s12 s \ length (s\ p1) > 0 \ butlast (s\ p1) = filter_on_channel \12 (hist s)" -definition Ip1_2 :: ex_pred where - "Ip1_2 \ \s. filter_on_channel \12 (hist s) \ s\ p1" - -definition Ip2_0 :: ex_pred where - "Ip2_0 \ \s. filter_on_channel \12 (hist s) = filter_on_channel \23 (hist s) @ s\ p2" -(* We would get this for free from a proper VCG. *) -definition Ip2_1 :: ex_pred where - "Ip2_1 \ \s. at p2 s23 s \ length (s\ p2) > 0" - -definition Ip3_0 :: ex_pred where - "Ip3_0 \ \s. s\ p3 = filter_on_channel \23 (hist s)" - -definition I_pred :: ex_pred where - "I_pred \ pred_conjoin [ Ip1_0, Ip1_1, Ip1_2, Ip2_0, Ip2_1, Ip3_0 ]" - -lemmas I_defs = I_pred_def Ip1_0_def Ip1_1_def Ip1_2_def Ip2_0_def Ip2_1_def Ip3_0_def - -text\ - -The local state of @{const "p3"} is some prefix of the local state of -@{const "p1"}. - -\ - -definition Etern_pred :: ex_pred where - "Etern_pred \ \s. s\ p3 \ s\ p1" - -lemma correct_system: - "I_pred s \ Etern_pred s" -(*<*) -by (clarsimp simp: Etern_pred_def I_defs less_eq_list_def prefix_def) - -lemma p1_c1[simplified, intro]: - "ex_pgms, p1, lconst (\l. l = s12) \ \I_pred\ \c1\ LocalOp (\xs. { xs @ [x] |x. True })" -apply (rule vcg.intros) -apply (clarsimp simp: I_defs atS_def) -done - -lemma p1_s12[intro]: - "ex_pgms, p1, lconst (\l. l = c1) \ \I_pred\ \s12\ \12\last" -apply (rule vcg.intros) -apply (rename_tac p') -apply (case_tac p', simp_all) -apply (clarsimp simp: I_defs atS_def elim!: butlastE) -done - -lemma p2_s23[intro]: - "ex_pgms, p2, lconst (\l. l = r12 \ l = \4) \ \I_pred\ \s23\ Request (\s. (\23, hd s)) (\ans s. {tl s})" -apply (rule vcg.intros) -apply (rename_tac p') -apply (case_tac p', simp_all) -apply (clarsimp simp: I_defs atS_def) -done - -lemma p2_pi4[intro]: - "ex_pgms, p2, lcond (\l. l = s23) (\l. l = r12 \ l = \4) \ \I_pred\ \\4\ IF \s. s \ [] THEN c' FI" -apply (rule vcg.intros) -apply (clarsimp simp: I_defs atS_def split: lcond_splits) -done - -(*>*) -text\\ - -lemma "s \ reachable_states ex_system \ I_pred (mkP s)" -(*<*) -apply (erule VCG) - apply (clarsimp dest!: initial_statesD simp: I_defs atS_def) -apply simp -apply (rename_tac p) -apply (case_tac p) - apply auto -done -(*>*) -(*<*) - -end -(*>*) diff --git a/thys/ConcurrentIMP/CIMP_vcg.thy b/thys/ConcurrentIMP/CIMP_vcg.thy --- a/thys/ConcurrentIMP/CIMP_vcg.thy +++ b/thys/ConcurrentIMP/CIMP_vcg.thy @@ -1,436 +1,793 @@ (*<*) (* * Copyright 2015, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) theory CIMP_vcg imports CIMP_lang begin (*>*) -subsection\Simple-minded Hoare Logic/VCG for CIMP\ +section\ State-based invariants \label{sec:cimp-invariants} \ + +text\ + +We provide a simple-minded verification condition generator (VCG) for this language, providing +support for establishing state-based invariants. It is just one way of reasoning about CIMP programs +and is proven sound wrt to the CIMP semantics. + +Our approach follows @{cite [cite_macro=citet] +"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"} +(and the later @{cite [cite_macro=citet] "Lamport:2002"}) and closely +related work by @{cite [cite_macro=citet] "AptFrancezDeRoever:1980"}, +@{cite [cite_macro=citet] "CousotCousot:1980"} and @{cite +[cite_macro=citet] "DBLP:journals/acta/LevinG81"}, who suggest the +incorporation of a history variable. @{cite [cite_macro=citet] +"CousotCousot:1980"} apparently contains a completeness proof. +Lamport mentions that this technique was well-known in the mid-80s +when he proposed the use of prophecy variables\footnote{@{url +"https://lamport.azurewebsites.net/pubs/pubs.html"}}. See also @{cite +[cite_macro=citet] "deRoeverEtAl:2001"} for an extended discussion of +some of this. + +\ + +declare small_step.intros[intro] + +inductive_cases small_step_inv: + "(\l\ Request action val # cs, ls) \\<^bsub>a\<^esub> s'" + "(\l\ Response action # cs, ls) \\<^bsub>a\<^esub> s'" + "(\l\ LocalOp R # cs, ls) \\<^bsub>a\<^esub> s'" + "(\l\ IF b THEN c FI # cs, ls) \\<^bsub>a\<^esub> s'" + "(\l\ IF b THEN c1 ELSE c2 FI # cs, ls) \\<^bsub>a\<^esub> s'" + "(\l\ WHILE b DO c OD # cs, ls) \\<^bsub>a\<^esub> s'" + "(LOOP DO c OD # cs, ls) \\<^bsub>a\<^esub> s'" + +lemma small_step_stuck: + "\ ([], s) \\<^bsub>\\<^esub> c'" +by (auto elim: small_step.cases) + +declare system_step.intros[intro] + +text\ + +By default we ask the simplifier to rewrite @{const "atS"} using +ambient @{const "AT"} information. + +\ + +lemma atS_state_weak_cong[cong]: + "AT s p = AT s' p \ atS p ls s \ atS p ls s'" +by (auto simp: atS_def) + +text\ + +We provide an incomplete set of basic rules for label sets. + +\ + +lemma atS_simps: + "\atS p {} s" + "atS p {l} s \ at p l s" + "\at p l s; l \ ls\ \ atS p ls s" + "(\l. at p l s \ l \ ls) \ \atS p ls s" +by (auto simp: atS_def) + +lemma atS_mono: + "\atS p ls s; ls \ ls'\ \ atS p ls' s" +by (auto simp: atS_def) + +lemma atS_un: + "atS p (l \ l') s \ atS p l s \ atS p l' s" +by (auto simp: atS_def) + +lemma atLs_disj_union[simp]: + "(atLs p label0 \<^bold>\ atLs p label1) = atLs p (label0 \ label1)" +unfolding atLs_def by simp + +lemma atLs_insert_disj: + "atLs p (insert l label0) = (atL p l \<^bold>\ atLs p label0)" +by simp + +lemma small_step_terminated: + "s \\<^bsub>x\<^esub> s' \ atCs (fst s) = {} \ atCs (fst s') = {}" +by (induct pred: small_step) auto + +lemma atC_not_empty: + "atC c \ {}" +by (induct c) auto + +lemma atCs_empty: + "atCs cs = {} \ cs = []" +by (induct cs) (auto simp: atC_not_empty) + +lemma terminated_no_commands: + assumes "terminated p sh" + shows "\s. GST sh p = ([], s)" +using assms unfolding atLs_def AT_def by (metis atCs_empty prod.collapse singletonD) + +lemma terminated_GST_stable: + assumes "system_step q sh' sh" + assumes "terminated p sh" + shows "GST sh p = GST sh' p" +using assms by (auto dest!: terminated_no_commands simp: small_step_stuck elim!: system_step.cases) + +lemma terminated_stable: + assumes "system_step q sh' sh" + assumes "terminated p sh" + shows "terminated p sh'" +using assms unfolding atLs_def AT_def +by (fastforce split: if_splits prod.splits + dest: small_step_terminated + elim!: system_step.cases) + +lemma system_step_pls_nonempty: + assumes "system_step pls sh' sh" + shows "pls \ {}" +using assms by cases simp_all + +lemma system_step_no_change: + assumes "system_step ps sh' sh" + assumes "p \ ps" + shows "GST sh' p = GST sh p" +using assms by cases simp_all + +lemma initial_stateD: + assumes "initial_state sys s" + shows "AT (\GST = s, HST = []\) = atC \ PGMs sys \ INIT sys (\GST = s, HST = []\)\ \ (\p l. \taken p l \GST = s, HST = []\)" +using assms unfolding initial_state_def split_def o_def LST_def AT_def taken_def by simp + +lemma initial_states_initial[iff]: + assumes "initial_state sys s" + shows "at p l (\GST = s, HST = []\) \ l \ atC (PGMs sys p)" +using assms unfolding initial_state_def split_def AT_def by simp + +definition + reachable_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext + \ ('answer, 'location, 'proc, 'question, 'state) state_pred" +where + "reachable_state sys s \ (\\ i. prerun sys \ \ \ i = s)" + +lemma reachable_stateE: + assumes "reachable_state sys sh" + assumes "\\ i. prerun sys \ \ P (\ i)" + shows "P sh" +using assms unfolding reachable_state_def by blast + +lemma prerun_reachable_state: + assumes "prerun sys \" + shows "reachable_state sys (\ i)" +using assms unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def by auto + +lemma reachable_state_induct[consumes 1, case_names init LocalStep CommunicationStep, induct set: reachable_state]: + assumes r: "reachable_state sys sh" + assumes i: "\s. initial_state sys s \ P \GST = s, HST = []\" + assumes l: "\sh ls' p. \reachable_state sys sh; P sh; GST sh p \\<^bsub>\\<^esub> ls'\ \ P \GST = (GST sh)(p := ls'), HST = HST sh\" + assumes c: "\sh ls1' ls2' p1 p2 \ \. + \reachable_state sys sh; P sh; + GST sh p1 \\<^bsub>\\, \\\<^esub> ls1'; GST sh p2 \\<^bsub>\\, \\\<^esub> ls2'; p1 \ p2 \ + \ P \GST = (GST sh)(p1 := ls1', p2 := ls2'), HST = HST sh @ [(\, \)]\" + shows "P sh" +using r +proof(rule reachable_stateE) + fix \ i assume "prerun sys \" show "P (\ i)" + proof(induct i) + case 0 from \prerun sys \\ show ?case + unfolding prerun_def by (metis (full_types) i old.unit.exhaust system_state.surjective) + next + case (Suc i) with \prerun sys \\ show ?case +unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def +apply clarsimp +apply (drule_tac x=i in spec) +apply (erule disjE; clarsimp) +apply (erule system_step.cases; clarsimp) + apply (metis (full_types) \prerun sys \\ l old.unit.exhaust prerun_reachable_state system_state.surjective) +apply (metis (full_types) \prerun sys \\ c old.unit.exhaust prerun_reachable_state system_state.surjective) +done + qed +qed + +lemma prerun_valid_TrueI: + shows "sys \\<^bsub>pre\<^esub> \True\" +unfolding prerun_valid_def by simp + +lemma prerun_valid_conjI: + assumes "sys \\<^bsub>pre\<^esub> P" + assumes "sys \\<^bsub>pre\<^esub> Q" + shows "sys \\<^bsub>pre\<^esub> P \<^bold>\ Q" +using assms unfolding prerun_valid_def always_def by simp + +lemma valid_prerun_lift: + assumes "sys \\<^bsub>pre\<^esub> I" + shows "sys \ \\I\" +using assms unfolding prerun_valid_def valid_def run_def by blast + +lemma prerun_valid_induct: + assumes "\\. prerun sys \ \ \I\ \" + assumes "\\. prerun sys \ \ (\I\ \<^bold>\ (\\I\)) \" + shows "sys \\<^bsub>pre\<^esub> I" +unfolding prerun_valid_def using assms by (simp add: always_induct) + +lemma prerun_validI: + assumes "\s. reachable_state sys s \ I s" + shows "sys \\<^bsub>pre\<^esub> I" +unfolding prerun_valid_def using assms by (simp add: alwaysI prerun_reachable_state) + +lemma prerun_validE: + assumes "reachable_state sys s" + assumes "sys \\<^bsub>pre\<^esub> I" + shows "I s" +using assms unfolding prerun_valid_def +by (metis alwaysE reachable_stateE suffix_state_prop) + + +subsubsection\Relating reachable states to the initial programs \label{sec:cimp-decompose-small-step}\ + +text\ + +To usefully reason about the control locations presumably embedded in +the single global invariant, we need to link the programs we have in +reachable state \s\ to the programs in the initial states. The +\fragments\ function decomposes the program into statements +that can be directly executed (\S\ref{sec:cimp-decompose}). We also +compute the locations we could be at after executing that statement as +a function of the process's local state. + +Eliding the bodies of \IF\ and \WHILE\ statements +yields smaller (but equivalent) proof obligations. + +\ + +type_synonym ('answer, 'location, 'question, 'state) loc_comp + = "'state \ 'location set" + +fun lconst :: "'location set \ ('answer, 'location, 'question, 'state) loc_comp" where + "lconst lp s = lp" + +definition lcond :: "'location set \ 'location set \ 'state bexp + \ ('answer, 'location, 'question, 'state) loc_comp" where + "lcond lp lp' b s = (if b s then lp else lp')" + +lemma lcond_split: + "Q (lcond lp lp' b s) \ (b s \ Q lp) \ (\b s \ Q lp')" +unfolding lcond_def by (simp split: if_splits) + +lemma lcond_split_asm: + "Q (lcond lp lp' b s) \ \ ((b s \ \Q lp) \ (\b s \ \ Q lp'))" +unfolding lcond_def by (simp split: if_splits) + +lemmas lcond_splits = lcond_split lcond_split_asm + +fun + fragments :: "('answer, 'location, 'question, 'state) com + \ 'location set + \ ( ('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'question, 'state) loc_comp ) set" +where + "fragments (\l\ IF b THEN c FI) aft + = { (\l\ IF b THEN c' FI, lcond (atC c) aft b) |c'. True } + \ fragments c aft" +| "fragments (\l\ IF b THEN c1 ELSE c2 FI) aft + = { (\l\ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True } + \ fragments c1 aft \ fragments c2 aft" +| "fragments (LOOP DO c OD) aft = fragments c (atC c)" +| "fragments (\l\ WHILE b DO c OD) aft + = fragments c {l} \ { (\l\ WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }" +| "fragments (c1;; c2) aft = fragments c1 (atC c2) \ fragments c2 aft" +| "fragments (c1 \ c2) aft = fragments c1 aft \ fragments c2 aft" +| "fragments c aft = { (c, lconst aft) }" + +fun + fragmentsL :: "('answer, 'location, 'question, 'state) com list + \ ( ('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'question, 'state) loc_comp ) set" +where + "fragmentsL [] = {}" +| "fragmentsL [c] = fragments c {}" +| "fragmentsL (c # c' # cs) = fragments c (atC c') \ fragmentsL (c' # cs)" + +abbreviation + fragmentsLS :: "('answer, 'location, 'question, 'state) local_state + \ ( ('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'question, 'state) loc_comp ) set" +where + "fragmentsLS s \ fragmentsL (cPGM s)" + +text\ + +We show that taking system steps preserves fragments. + +\ + +lemma small_step_fragmentsLS: + assumes "s \\<^bsub>\\<^esub> s'" + shows "fragmentsLS s' \ fragmentsLS s" +using assms by induct (case_tac [!] cs, auto) + +lemma reachable_state_fragmentsLS: + assumes "reachable_state sys sh" + shows "fragmentsLS (GST sh p) \ fragments (PGMs sys p) {}" +using assms +by (induct rule: reachable_state_induct) + (auto simp: initial_state_def dest: subsetD[OF small_step_fragmentsLS]) + +inductive + basic_com :: "('answer, 'location, 'question, 'state) com \ bool" +where + "basic_com (\l\ Request action val)" +| "basic_com (\l\ Response action)" +| "basic_com (\l\ LocalOp R)" +| "basic_com (\l\ IF b THEN c FI)" +| "basic_com (\l\ IF b THEN c1 ELSE c2 FI)" +| "basic_com (\l\ WHILE b DO c OD)" + +lemma fragments_basic_com: + assumes "(c', aft') \ fragments c aft" + shows "basic_com c'" +using assms by (induct c arbitrary: aft) (auto intro: basic_com.intros) + +lemma fragmentsL_basic_com: + assumes "(c', aft') \ fragmentsL cs" + shows "basic_com c'" +using assms +apply (induct cs) + apply simp +apply (case_tac cs) + apply (auto simp: fragments_basic_com) +done + +text\ + +To reason about system transitions we need to identify which basic +statement gets executed next. To that end we factor out the recursive +cases of the @{term "small_step"} semantics into \emph{contexts}, +which isolate the \basic_com\ commands with immediate +externally-visible behaviour. Note that non-determinism means that +more than one \basic_com\ can be enabled at a time. + +The representation of evaluation contexts follows @{cite +[cite_macro=citet] "DBLP:journals/jar/Berghofer12"}. This style of +operational semantics was originated by @{cite [cite_macro=citet] +"FelleisenHieb:1992"}. + +\ + +type_synonym ('answer, 'location, 'question, 'state) ctxt + = "(('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com) + \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com list)" + +inductive_set + ctxt :: "('answer, 'location, 'question, 'state) ctxt set" +where + C_Hole: "(id, \[]\) \ ctxt" +| C_Loop: "(E, fctxt) \ ctxt \ (\c1. LOOP DO E c1 OD, \c1. fctxt c1 @ [LOOP DO E c1 OD]) \ ctxt" +| C_Seq: "(E, fctxt) \ ctxt \ (\c1. E c1;; c2, \c1. fctxt c1 @ [c2]) \ ctxt" +| C_Choose1: "(E, fctxt) \ ctxt \ (\c1. E c1 \ c2, fctxt) \ ctxt" +| C_Choose2: "(E, fctxt) \ ctxt \ (\c2. c1 \ E c2, fctxt) \ ctxt" + +text\ + +We can decompose a small step into a context and a @{const "basic_com"}. + +\ + +fun + decompose_com :: "('answer, 'location, 'question, 'state) com + \ ( ('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'question, 'state) ctxt ) set" +where + "decompose_com (LOOP DO c1 OD) = { (c, \t. LOOP DO ictxt t OD, \t. fctxt t @ [LOOP DO ictxt t OD]) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 }" +| "decompose_com (c1;; c2) = { (c, \t. ictxt t;; c2, \t. fctxt t @ [c2]) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 }" +| "decompose_com (c1 \ c2) = { (c, \t. ictxt t \ c2, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c1 } + \ { (c, \t. c1 \ ictxt t, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) \ decompose_com c2 }" +| "decompose_com c = {(c, id, \[]\)}" + +definition + decomposeLS :: "('answer, 'location, 'question, 'state) local_state + \ ( ('answer, 'location, 'question, 'state) com + \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com) + \ (('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) com list) ) set" +where + "decomposeLS s = (case cPGM s of c # _ \ decompose_com c | _ \ {})" + +lemma ctxt_inj: + assumes "(E, fctxt) \ ctxt" + assumes "E x = E y" + shows "x = y" +using assms by (induct set: ctxt) auto + +lemma decompose_com_non_empty: "decompose_com c \ {}" +by (induct c) auto + +lemma decompose_com_basic_com: + assumes "(c', ctxts) \ decompose_com c" + shows "basic_com c'" +using assms by (induct c arbitrary: c' ctxts) (auto intro: basic_com.intros) + +lemma decomposeLS_basic_com: + assumes "(c', ctxts) \ decomposeLS s" + shows "basic_com c'" +using assms unfolding decomposeLS_def by (simp add: decompose_com_basic_com split: list.splits) + +lemma decompose_com_ctxt: + assumes "(c', ctxts) \ decompose_com c" + shows "ctxts \ ctxt" +using assms by (induct c arbitrary: c' ctxts) (auto intro: ctxt.intros) + +lemma decompose_com_ictxt: + assumes "(c', ictxt, fctxt) \ decompose_com c" + shows "ictxt c' = c" +using assms by (induct c arbitrary: c' ictxt fctxt) auto + +lemma decompose_com_small_step: + assumes as: "(c' # fctxt c' @ cs, s) \\<^bsub>\\<^esub> s'" + assumes ds: "(c', ictxt, fctxt) \ decompose_com c" + shows "(c # cs, s) \\<^bsub>\\<^esub> s'" +using decompose_com_ctxt[OF ds] as decompose_com_ictxt[OF ds] +by (induct ictxt fctxt arbitrary: c cs) + (cases s', fastforce simp: fun_eq_iff dest: ctxt_inj)+ + +theorem context_decompose: + "s \\<^bsub>\\<^esub> s' \ (\(c, ictxt, fctxt) \ decomposeLS s. + cPGM s = ictxt c # tl (cPGM s) + \ (c # fctxt c @ tl (cPGM s), cTKN s, cLST s) \\<^bsub>\\<^esub> s' + \ (\l\atC c. cTKN s' = Some l))" (is "?lhs = ?rhs") +proof(rule iffI) + assume ?lhs then show ?rhs + unfolding decomposeLS_def + proof(induct rule: small_step.induct) + case (Choose1 c1 cs s \ cs' s' c2) then show ?case + apply clarsimp + apply (rename_tac c ictxt fctxt) + apply (rule_tac x="(c, \t. ictxt t \ c2, fctxt)" in bexI) + apply auto + done + next + case (Choose2 c2 cs s \ cs' s' c1) then show ?case + apply clarsimp + apply (rename_tac c ictxt fctxt) + apply (rule_tac x="(c, \t. c1 \ ictxt t, fctxt)" in bexI) + apply auto + done + qed fastforce+ +next + assume ?rhs then show ?lhs + unfolding decomposeLS_def + by (cases s) (auto split: list.splits dest: decompose_com_small_step) +qed + +text\ + +While we only use this result left-to-right (to decompose a small step +into a basic one), this equivalence shows that we lose no information +in doing so. + +Decomposing a compound command preserves @{const \fragments\} too. + +\ + +fun + loc_compC :: "('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'question, 'state) com list + \ ('answer, 'location, 'question, 'state) loc_comp" +where + "loc_compC (\l\ IF b THEN c FI) cs = lcond (atC c) (atCs cs) b" +| "loc_compC (\l\ IF b THEN c1 ELSE c2 FI) cs = lcond (atC c1) (atC c2) b" +| "loc_compC (LOOP DO c OD) cs = lconst (atC c)" +| "loc_compC (\l\ WHILE b DO c OD) cs = lcond (atC c) (atCs cs) b" +| "loc_compC c cs = lconst (atCs cs)" + +lemma decompose_fragments: + assumes "(c, ictxt, fctxt) \ decompose_com c0" + shows "(c, loc_compC c (fctxt c @ cs)) \ fragments c0 (atCs cs)" +using assms +proof(induct c0 arbitrary: c ictxt fctxt cs) + case (Loop c01 c ictxt fctxt cs) + from Loop.prems Loop.hyps(1)[where cs="ictxt c # cs"] show ?case by (auto simp: decompose_com_ictxt) +next + case (Seq c01 c02 c ictxt fctxt cs) + from Seq.prems Seq.hyps(1)[where cs="c02 # cs"] show ?case by auto +qed auto + +lemma at_decompose: + assumes "(c, ictxt, fctxt) \ decompose_com c0" + shows "atC c \ atC c0" +using assms by (induct c0 arbitrary: c ictxt fctxt; fastforce) + +lemma at_decomposeLS: + assumes "(c, ictxt, fctxt) \ decomposeLS s" + shows "atC c \ atCs (cPGM s)" +using assms unfolding decomposeLS_def by (auto simp: at_decompose split: list.splits) + +lemma decomposeLS_fragmentsLS: + assumes "(c, ictxt, fctxt) \ decomposeLS s" + shows "(c, loc_compC c (fctxt c @ tl (cPGM s))) \ fragmentsLS s" +using assms +proof(cases "cPGM s") + case (Cons d ds) + with assms decompose_fragments[where cs="ds"] show ?thesis + by (cases ds) (auto simp: decomposeLS_def) +qed (simp add: decomposeLS_def) + +lemma small_step_loc_compC: + assumes "basic_com c" + assumes "(c # cs, ls) \\<^bsub>\\<^esub> ls'" + shows "loc_compC c cs (snd ls) = atCs (cPGM ls')" +using assms by (fastforce elim: basic_com.cases elim!: small_step_inv split: lcond_splits) + +text\ + +The headline result allows us to constrain the initial and final states +of a given small step in terms of the original programs, provided the +initial state is reachable. + +\ + +theorem decompose_small_step: + assumes "GST sh p \\<^bsub>\\<^esub> ps'" + assumes "reachable_state sys sh" + obtains c cs aft + where "(c, aft) \ fragments (PGMs sys p) {}" + and "atC c \ atCs (cPGM (GST sh p))" + and "aft (cLST (GST sh p)) = atCs (cPGM ps')" + and "(c # cs, cTKN (GST sh p), cLST (GST sh p)) \\<^bsub>\\<^esub> ps'" + and "\l\atC c. cTKN ps' = Some l" +using assms +apply - +apply (frule iffD1[OF context_decompose]) +apply clarsimp +apply (frule decomposeLS_fragmentsLS) +apply (frule at_decomposeLS) +apply (frule (1) subsetD[OF reachable_state_fragmentsLS]) +apply (frule decomposeLS_basic_com) +apply (frule (1) small_step_loc_compC) +apply simp +done + +text\ + +Reasoning by induction over the reachable states +with @{thm [source] "decompose_small_step"} is quite tedious. We +provide a very simple VCG that generates friendlier local proof +obligations in \S\ref{sec:vcg}. + +\ + + +subsection\Simple-minded Hoare Logic/VCG for CIMP \label{sec:vcg}\ text\ \label{sec:cimp-vcg} We do not develop a proper Hoare logic or full VCG for CIMP: this machinery merely packages up the subgoals that arise from induction over the reachable states (\S\ref{sec:cimp-invariants}). This is somewhat in the spirit of @{cite [cite_macro=citet] "Ridge:2009"}. Note that this approach is not compositional: it consults the original system to find matching communicating pairs, and \aft\ tracks the labels of possible successor statements. More serious Hoare logics are provided by @{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84" and "CousotCousot89-IC"}. Intuitively we need to discharge a proof obligation for either @{const "Request"}s or @{const "Response"}s but not both. Here we choose to focus on @{const "Request"}s as we expect to have more local information available about these. \ inductive vcg :: "('answer, 'location, 'proc, 'question, 'state) programs \ 'proc \ ('answer, 'location, 'question, 'state) loc_comp - \ ('answer, 'location, 'proc, 'question, 'state) pred + \ ('answer, 'location, 'proc, 'question, 'state) state_pred \ ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'proc, 'question, 'state) pred - \ bool" ("_, _, _ \/ \_\/ _/ \_\") + \ ('answer, 'location, 'proc, 'question, 'state) state_pred + \ bool" ("_, _, _ \/ \_\/ _/ \_\" [11,0,0,0,0,0] 11) where - Request: "\ \aft' action' s ps' p's' l' \ s' p'. - \ pre s; (\l'\ Response action', aft') \ fragments (pgms p') \False\; p \ p'; - ps' \ val \ (LST s p); (p's', \) \ action' (action (LST s p)) (LST s p'); - at p l s; at p' l' s; - AT s' = (AT s)(p := aft (\l\ Request action val) (LST s p), - p' := aft' (\l'\ Response action') (LST s p')); - LST s' = (LST s)(p := ps', p' := p's'); - hist s' = hist s @ [(action (LST s p), \)] - \ \ post s' - \ \ pgms, p, aft \ \pre\ \l\ Request action val \post\" -| LocalOp: "\ \s ps' s'. \ pre s; ps' \ f (LST s p); - at p l s; - AT s' = (AT s)(p := aft (\l\ LocalOp f) (LST s p)); - LST s' = (LST s)(p := ps'); - hist s' = hist s - \ \ post s' - \ \ pgms, p, aft \ \pre\ \l\ LocalOp f \post\" -| Cond1: "\ \s s'. \ pre s; - at p l s; - AT s' = (AT s)(p := aft (\l\ IF b THEN t FI) (LST s p)); - LST s' = LST s; - hist s' = hist s - \ \ post s' - \ \ pgms, p, aft \ \pre\ \l\ IF b THEN t FI \post\" -| Cond2: "\ \s s'. \ pre s; - at p l s; - AT s' = (AT s)(p := aft (\l\ IF b THEN t ELSE e FI) (LST s p)); - LST s' = LST s; - hist s' = hist s - \ \ post s' - \ \ pgms, p, aft \ \pre\ \l\ IF b THEN t ELSE e FI \post\" -| While: "\ \s s'. \ pre s; - at p l s; - AT s' = (AT s)(p := aft (\l\ WHILE b DO c OD) (LST s p)); - LST s' = LST s; - hist s' = hist s - \ \ post s' - \ \ pgms, p, aft \ \pre\ \l\ WHILE b DO c OD \post\" -\ \There are no proof obligations for the following commands.\ -| Response: "pgms, p, aft \ \pre\ \l\ Response action \post\" -| Seq: "pgms, p, aft \ \pre\ c1 ;; c2 \post\" -| Loop: "pgms, p, aft \ \pre\ LOOP DO c OD \post\" -| Choose: "pgms, p, aft \ \pre\ c1 \ c2 \post\" + "\ \aft' action' s ps' p's' l' \ s' p'. + \ pre s; (\l'\ Response action', aft') \ fragments (coms p') {}; p \ p'; + ps' \ val \ (s\ p); (p's', \) \ action' (action (s\ p)) (s\ p'); + at p l s; at p' l' s; + AT s' = (AT s)(p := aft (s\ p), p' := aft' (s\ p')); + s'\ = s\(p := ps', p' := p's'); + taken p l s'; + HST s' = HST s @ [(action (s\ p), \)]; + \p''\-{p,p'}. GST s' p'' = GST s p'' + \ \ post s' + \ \ coms, p, aft \ \pre\ \l\ Request action val \post\" +| "\ \s ps' s'. + \ pre s; ps' \ f (s\ p); + at p l s; + AT s' = (AT s)(p := aft (s\ p)); + s'\ = s\(p := ps'); + taken p l s'; + HST s' = HST s; + \p''\-{p}. GST s' p'' = GST s p'' + \ \ post s' + \ \ coms, p, aft \ \pre\ \l\ LocalOp f \post\" +| "\ \s s'. + \ pre s; + at p l s; + AT s' = (AT s)(p := aft (s\ p)); + s'\ = s\; + taken p l s'; + HST s' = HST s; + \p''\-{p}. GST s' p'' = GST s p'' + \ \ post s' + \ \ coms, p, aft \ \pre\ \l\ IF b THEN t FI \post\" +| "\ \s s'. + \ pre s; + at p l s; + AT s' = (AT s)(p := aft (s\ p)); + s'\ = s\; + taken p l s'; + HST s' = HST s; + \p''\-{p}. GST s' p'' = GST s p'' + \ \ post s' + \ \ coms, p, aft \ \pre\ \l\ IF b THEN t ELSE e FI \post\" +| "\ \s s'. + \ pre s; + at p l s; + AT s' = (AT s)(p := aft (s\ p)); + s'\ = s\; + taken p l s'; + HST s' = HST s; + \p''\-{p}. GST s' p'' = GST s p'' + \ \ post s' + \ \ coms, p, aft \ \pre\ \l\ WHILE b DO c OD \post\" +\ \There are no proof obligations for the following commands, but including them makes some basic rules hold (\S\ref{sec:cimp:vcg_rules}):\ +| "coms, p, aft \ \pre\ \l\ Response action \post\" +| "coms, p, aft \ \pre\ c1 ;; c2 \post\" +| "coms, p, aft \ \pre\ LOOP DO c OD \post\" +| "coms, p, aft \ \pre\ c1 \ c2 \post\" text\ We abbreviate invariance with one-sided validity syntax. \ -abbreviation valid_inv ("_, _, _ \/ \_\/ _") where - "pgms, p, aft \ \I\ c \ pgms, p, aft \ \I\ c \I\" -(*<*) +abbreviation valid_inv ("_, _, _ \/ \_\/ _" [11,0,0,0,0] 11) where + "coms, p, aft \ \I\ c \ coms, p, aft \ \I\ c \I\" inductive_cases vcg_inv: - "pgms, p, aft \ \pre\ \l\ Request action val \post\" - "pgms, p, aft \ \pre\ \l\ LocalOp f \post\" - "pgms, p, aft \ \pre\ \l\ IF b THEN t FI \post\" - "pgms, p, aft \ \pre\ \l\ IF b THEN t ELSE e FI \post\" - "pgms, p, aft \ \pre\ LOOP DO c OD \post\" - "pgms, p, aft \ \pre\ \l\ WHILE b DO c OD \post\" - "pgms, p, aft \ \pre\ \l\ Response action \post\" - "pgms, p, aft \ \pre\ c1 ;; c2 \post\" - "pgms, p, aft \ \pre\ c1 \ c2 \post\" + "coms, p, aft \ \pre\ \l\ Request action val \post\" + "coms, p, aft \ \pre\ \l\ LocalOp f \post\" + "coms, p, aft \ \pre\ \l\ IF b THEN t FI \post\" + "coms, p, aft \ \pre\ \l\ IF b THEN t ELSE e FI \post\" + "coms, p, aft \ \pre\ \l\ WHILE b DO c OD \post\" + "coms, p, aft \ \pre\ LOOP DO c OD \post\" + "coms, p, aft \ \pre\ \l\ Response action \post\" + "coms, p, aft \ \pre\ c1 ;; c2 \post\" + "coms, p, aft \ \pre\ Choose c1 c2 \post\" -lemma vcg_precond_cong: - "P = P' \ (pgms, p, aft \ \P\ c \Q\) \ (pgms, p, aft \ \P'\ c \Q\)" -by simp - -lemma vcg_postcond_cong: - "Q = Q' \ (pgms, p, aft \ \P\ c \Q\) \ (pgms, p, aft \ \P\ c \Q'\)" -by simp - -(*>*) text\ We tweak @{const "fragments"} by omitting @{const "Response"}s, -yielding fewer obligations. +yielding fewer obligations \ fun vcg_fragments' :: "('answer, 'location, 'question, 'state) com - \ ('location \ bool) + \ 'location set \ ( ('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) loc_comp ) set" where - "vcg_fragments' (\l\ Response action) ls = {}" -| "vcg_fragments' (\l\ IF b THEN c FI) ls - = vcg_fragments' c ls - \ { (\l\ IF b THEN c' FI, lcond (atC c) ls) |c'. True }" -| "vcg_fragments' (\l\ IF b THEN c1 ELSE c2 FI) ls - = vcg_fragments' c2 ls \ vcg_fragments' c1 ls - \ { (\l\ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2)) |c1' c2'. True }" -| "vcg_fragments' (LOOP DO c OD) ls = vcg_fragments' c (atC c)" -| "vcg_fragments' (\l'\ WHILE b DO c OD) ls - = vcg_fragments' c (\l. l = l') \ { (\l'\ WHILE b DO c' OD, lcond (atC c) ls) |c'. True }" -| "vcg_fragments' (c1 ;; c2) ls = vcg_fragments' c2 ls \ vcg_fragments' c1 (atC c2)" -| "vcg_fragments' (c1 \ c2) ls = vcg_fragments' c1 ls \ vcg_fragments' c2 ls" -| "vcg_fragments' c ls = {(c, lconst ls)}" + "vcg_fragments' (\l\ Response action) aft = {}" +| "vcg_fragments' (\l\ IF b THEN c FI) aft + = vcg_fragments' c aft + \ { (\l\ IF b THEN c' FI, lcond (atC c) aft b) |c'. True }" +| "vcg_fragments' (\l\ IF b THEN c1 ELSE c2 FI) aft + = vcg_fragments' c2 aft \ vcg_fragments' c1 aft + \ { (\l\ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True }" +| "vcg_fragments' (LOOP DO c OD) aft = vcg_fragments' c (atC c)" +| "vcg_fragments' (\l\ WHILE b DO c OD) aft + = vcg_fragments' c {l} \ { (\l\ WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }" +| "vcg_fragments' (c1 ;; c2) aft = vcg_fragments' c2 aft \ vcg_fragments' c1 (atC c2)" +| "vcg_fragments' (c1 \ c2) aft = vcg_fragments' c1 aft \ vcg_fragments' c2 aft" +| "vcg_fragments' c aft = {(c, lconst aft)}" abbreviation vcg_fragments :: "('answer, 'location, 'question, 'state) com \ ( ('answer, 'location, 'question, 'state) com \ ('answer, 'location, 'question, 'state) loc_comp ) set" where - "vcg_fragments c \ vcg_fragments' c \False\" -(*<*) + "vcg_fragments c \ vcg_fragments' c {}" -lemma vcg_fragments'_inc: - "\ (c', lp) \ fragments c ls; \l action. c' \ \l\ Response action \ \ (c', lp) \ vcg_fragments' c ls" -by (induct c arbitrary: ls) (auto split: if_splits) +fun isResponse :: "('answer, 'location, 'question, 'state) com \ bool" where + "isResponse (\l\ Response action) \ True" +| "isResponse _ \ False" + +lemma fragments_vcg_fragments': + "\ (c, aft) \ fragments c' aft'; \isResponse c \ \ (c, aft) \ vcg_fragments' c' aft'" +by (induct c' arbitrary: aft') auto + +lemma vcg_fragments'_fragments: + "vcg_fragments' c' aft' \ fragments c' aft'" +by (induct c' arbitrary: aft') (auto 10 0) lemma VCG_step: - assumes V: "\p. \(c, afts) \ vcg_fragments (fst sys p). ((fst sys), p, afts \ \pre\ c \post\)" - assumes S: "(s, h) s\ (s', h')" - assumes R: "(s, h) \ reachable_states sys" - assumes P: "pre (mkP (s, h))" - shows "post (mkP (s', h'))" + assumes V: "\p. \(c, aft) \ vcg_fragments (PGMs sys p). PGMs sys, p, aft \ \pre\ c \post\" + assumes S: "system_step p sh' sh" + assumes R: "reachable_state sys sh" + assumes P: "pre sh" + shows "post sh'" using S proof cases - case (LocalStep p ps') with P show ?thesis + case LocalStep with P show ?thesis apply - apply (erule decompose_small_step[OF _ R]) - apply (elim basic_com.cases, simp_all) - apply (fastforce dest!: V[rule_format] vcg_fragments'_inc - elim!: small_step_inv vcg_inv - simp: fun_eq_iff LST_def AT_def mkP_def split_def)+ + apply (frule fragments_basic_com) + apply (erule basic_com.cases) + apply (fastforce dest!: fragments_vcg_fragments' V[rule_format] + elim: vcg_inv elim!: small_step_inv + simp: LST_def AT_def taken_def fun_eq_iff)+ done next - case (CommunicationStep p1 \ \ ls1' p2 ls2) with P show ?thesis + case CommunicationStep with P show ?thesis apply - apply (erule decompose_small_step[OF _ R]) apply (erule decompose_small_step[OF _ R]) - apply (elim basic_com.cases, simp_all) - apply (drule vcg_fragments'_inc, simp) - apply (drule V[rule_format]) - apply clarsimp - apply (erule vcg_inv) - apply (elim small_step_inv) - apply (fastforce simp add: fun_eq_iff LST_def AT_def mkP_def split_def) + subgoal for c cs aft c' cs' aft' + apply (frule fragments_basic_com[where c'=c]) + apply (frule fragments_basic_com[where c'=c']) + apply (elim basic_com.cases; clarsimp elim!: small_step_inv) + apply (drule fragments_vcg_fragments') + apply (fastforce dest!: V[rule_format] + elim: vcg_inv elim!: small_step_inv + simp: LST_def AT_def taken_def fun_eq_iff)+ + done done qed -(*>*) text\ -The user sees the conclusion of \V\ for each element of \vcg_fragments\. - -\ - -lemma VCG: - assumes R: "s \ reachable_states sys" - assumes I: "\s \ initial_states sys. I (mkP (s, []))" - assumes V: "\p. \(c, afts) \ vcg_fragments (fst sys p). ((fst sys), p, afts \ \I\ c)" - shows "I (mkP s)" -(*<*) -proof - - have "I (mkP (s', h'))" if B: "s0 \ initial_states sys" and S: "(s0, []) s\\<^sup>* (s', h')" for s0 s' h' - using S - proof(induct rule: rtrancl_induct2) - case refl with B show ?case by (rule I[rule_format]) - next - case (step s' h' s'' h'') with B V show ?case - by - (erule (1) VCG_step; auto simp: reachable_states_def) - qed - with I R show ?thesis by (cases s) (clarsimp simp: reachable_states_def) -qed -(*>*) - -subsubsection\VCG rules\ - -text\ - -We can develop some (but not all) of the familiar Hoare rules; see -@{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80"} and the -seL4/l4.verified lemma buckets for inspiration. We avoid many of the -issues Lamport mentions as we only treat basic (atomic) commands. +The user sees the conclusion of \V\ for each element of @{const \vcg_fragments\}. \ -context - fixes pgms :: "('answer, 'location, 'proc, 'question, 'state) programs" - fixes p :: "'proc" - fixes afts :: "('answer, 'location, 'question, 'state) loc_comp" -begin - -abbreviation - valid_syn :: "('answer, 'location, 'proc, 'question, 'state) pred - \ ('answer, 'location, 'question, 'state) com - \ ('answer, 'location, 'proc, 'question, 'state) pred \ bool" where - "valid_syn P c Q \ pgms, p, afts \ \P\ c \Q\" -notation valid_syn ("\_\/ _/ \_\") - -abbreviation - valid_inv_syn :: "('answer, 'location, 'proc, 'question, 'state) pred - \ ('answer, 'location, 'question, 'state) com \ bool" where - "valid_inv_syn P c \ \P\ c \P\" -notation valid_inv_syn ("\_\/ _") - -lemma vcg_True: - "\P\ c \\True\\" -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_conj: - "\ \I\ c \Q\; \I\ c \R\ \ \ \I\ c \Q \<^bold>\ R\" -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_pre_imp: - "\ \s. P s \ Q s; \Q\ c \R\ \ \ \P\ c \R\" -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemmas vcg_pre = vcg_pre_imp[rotated] - -lemma vcg_post_imp: - "\ \s. Q s \ R s; \P\ c \Q\ \ \ \P\ c \R\" -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_prop[intro]: - "\\P\\ c" -by (cases c) (fastforce intro: vcg.intros)+ - -lemma vcg_drop_imp: - assumes "\P\ c \Q\" - shows "\P\ c \R \<^bold>\ Q\" -using assms -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_conj_lift: - assumes x: "\P\ c \Q\" - assumes y: "\P'\ c \Q'\" - shows "\P \<^bold>\ P'\ c \Q \<^bold>\ Q'\" -apply (rule vcg_conj) - apply (rule vcg_pre[OF x], simp) -apply (rule vcg_pre[OF y], simp) +lemma VCG_step_inv_stable: + assumes V: "\p. \(c, aft) \ vcg_fragments (PGMs sys p). PGMs sys, p, aft \ \I\ c" + assumes "prerun sys \" + shows "(\I\ \<^bold>\ \\I\) \" +apply (rule alwaysI) +apply clarsimp +apply (rule nextI) +apply clarsimp +using assms(2) unfolding prerun_def +apply clarsimp +apply (erule_tac i=i in alwaysE) +unfolding system_step_reflclp_def +apply clarsimp +apply (erule disjE; clarsimp) +using VCG_step[where pre=I and post=I] V assms(2) prerun_reachable_state +apply blast done -lemma vcg_disj_lift: - assumes x: "\P\ c \Q\" - assumes y: "\P'\ c \Q'\" - shows "\P \<^bold>\ P'\ c \Q \<^bold>\ Q'\" -using assms -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_imp_lift: - assumes "\P'\ c \\<^bold>\ P\" - assumes "\Q'\ c \Q\" - shows "\P' \<^bold>\ Q'\ c \P \<^bold>\ Q\" -by (simp only: imp_conv_disj vcg_disj_lift[OF assms]) - -lemma vcg_ex_lift: - assumes "\x. \P x\ c \Q x\" - shows "\\s. \x. P x s\ c \\s. \x. Q x s\" -using assms -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_all_lift: - assumes "\x. \P x\ c \Q x\" - shows "\\s. \x. P x s\ c \\s. \x. Q x s\" -using assms -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_name_pre_state: - assumes "\s. P s \ \(=) s\ c \Q\" - shows "\P\ c \Q\" -using assms -by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ - -lemma vcg_lift_comp: - assumes f: "\P. \\s. P (f s :: 'a :: type)\ c" - assumes P: "\x. \Q x\ c \P x\" - shows "\\s. Q (f s) s\ c \\s. P (f s) s\" - apply (rule vcg_name_pre_state) - apply (rename_tac s) - apply (rule vcg_pre) - apply (rule vcg_post_imp[rotated]) - apply (rule vcg_conj_lift) - apply (rule_tac x="f s" in P) - apply (rule_tac P="\fs. fs = f s" in f) - apply simp - apply simp - done - -(* **************************************** *) - -subsubsection\Cheap non-interference rules\ - -text\ - -These rules magically construct VCG lifting rules from the easier to -prove \eq_imp\ facts. We don't actually use these in the GC, -but we do derive @{const "fun_upd"} equations using the same -mechanism. Thanks to Thomas Sewell for the requisite syntax magic. - -As these \eq_imp\ facts do not usefully compose, we make the -definition asymmetric (i.e., \g\ does not get a bundle of -parameters). - -\ - -definition eq_imp :: "('a \ 'b \ 'c) \ ('b \ 'e) \ bool" where - "eq_imp f g \ (\s s'. (\x. f x s = f x s') \ (g s = g s'))" - -lemma eq_impD: - "\ eq_imp f g; \x. f x s = f x s' \ \ g s = g s'" -by (simp add: eq_imp_def) - -lemma eq_imp_vcg: - assumes g: "eq_imp f g" - assumes f: "\x P. \P \ (f x)\ c" - shows "\P \ g\ c" - apply (rule vcg_name_pre_state) - apply (rename_tac s) - apply (rule vcg_pre) - apply (rule vcg_post_imp[rotated]) - apply (rule vcg_all_lift[where 'a='a]) - apply (rule_tac x=x and P="\fs. fs = f x s" in f[rule_format]) - apply simp - apply (frule eq_impD[where f=f, OF g]) - apply simp - apply simp - done - -lemma eq_imp_vcg_LST: - assumes g: "eq_imp f g" - assumes f: "\x P. \P \ (f x) \ LST\ c" - shows "\P \ g \ LST\ c" - apply (rule vcg_name_pre_state) - apply (rename_tac s) - apply (rule vcg_pre) - apply (rule vcg_post_imp[rotated]) - apply (rule vcg_all_lift[where 'a='a]) - apply (rule_tac x=x and P="\fs. fs = f x s\" in f[rule_format]) - apply simp - apply (frule eq_impD[where f=f, OF g]) - apply simp - apply simp - done - -lemma eq_imp_fun_upd: - assumes g: "eq_imp f g" - assumes f: "\x. f x (s(fld := val)) = f x s" - shows "g (s(fld := val)) = g s" -apply (rule eq_impD[OF g]) -apply (rule f) +lemma VCG: + assumes I: "\s. initial_state sys s \ I (\GST = s, HST = []\)" + assumes V: "\p. \(c, aft) \ vcg_fragments (PGMs sys p). PGMs sys, p, aft \ \I\ c" + shows "sys \\<^bsub>pre\<^esub> I" +apply (rule prerun_valid_induct) + apply (clarsimp simp: prerun_def state_prop_def) + apply (metis (full_types) I old.unit.exhaust system_state.surjective) +using VCG_step_inv_stable[OF V] apply blast done -lemma curry_forall_eq: - "(\f. P f) = (\f. P (case_prod f))" - apply safe - apply simp_all - apply (rename_tac f) - apply (drule_tac x="\x y. f (x, y)" in spec) - apply simp - done - -lemma pres_tuple_vcg: - "(\P. \P \ (\s. (f s, g s))\ c) - \ ((\P. \P \ f\ c) \ (\P. \P \ g\ c))" - apply (simp add: curry_forall_eq o_def) - apply safe - apply fast - apply fast - apply (rename_tac P) - apply (rule_tac f="f" and P="\fs s. P fs (g s)" in vcg_lift_comp, simp, simp) - done - -lemma pres_tuple_vcg_LST: - "(\P. \P \ (\s. (f s, g s)) \ LST\ c) - \ ((\P. \P \ f \ LST\ c) \ (\P. \P \ g \ LST\ c))" - apply (simp add: curry_forall_eq o_def) - apply safe - apply fast - apply fast - apply (rename_tac P) - apply (rule_tac f="\s. f s\" and P="\fs s. P fs (g s)" for g in vcg_lift_comp, simp, simp) - done - -lemmas conj_explode = conj_imp_eq_imp_imp - -end +lemmas VCG_valid = valid_prerun_lift[OF VCG, of sys I] for sys I (*<*) end (*>*) diff --git a/thys/ConcurrentIMP/CIMP_vcg_rules.thy b/thys/ConcurrentIMP/CIMP_vcg_rules.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/CIMP_vcg_rules.thy @@ -0,0 +1,229 @@ +(*<*) +(* + * Copyright 2015, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +theory CIMP_vcg_rules +imports + CIMP_vcg +begin + +(*>*) +subsubsection\ VCG rules \label{sec:cimp:vcg_rules} \ + +text\ + +We can develop some (but not all) of the familiar Hoare rules; see +@{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80"} and the +seL4/l4.verified lemma buckets for inspiration. We avoid many of the +issues Lamport mentions as we only treat basic (atomic) commands. + +\ + +context + fixes coms :: "('answer, 'location, 'proc, 'question, 'state) programs" + fixes p :: "'proc" + fixes aft :: "('answer, 'location, 'question, 'state) loc_comp" +begin + +abbreviation + valid_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred + \ ('answer, 'location, 'question, 'state) com + \ ('answer, 'location, 'proc, 'question, 'state) state_pred \ bool" where + "valid_syn P c Q \ coms, p, aft \ \P\ c \Q\" +notation valid_syn ("\_\/ _/ \_\") + +abbreviation + valid_inv_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred + \ ('answer, 'location, 'question, 'state) com \ bool" where + "valid_inv_syn P c \ \P\ c \P\" +notation valid_inv_syn ("\_\/ _") + +lemma vcg_True: + "\P\ c \\True\\" +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_conj: + "\ \I\ c \Q\; \I\ c \R\ \ \ \I\ c \Q \<^bold>\ R\" +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_pre_imp: + "\ \s. P s \ Q s; \Q\ c \R\ \ \ \P\ c \R\" +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemmas vcg_pre = vcg_pre_imp[rotated] + +lemma vcg_post_imp: + "\ \s. Q s \ R s; \P\ c \Q\ \ \ \P\ c \R\" +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_prop[intro]: + "\\P\\ c" +by (cases c) (fastforce intro: vcg.intros)+ + +lemma vcg_drop_imp: + assumes "\P\ c \Q\" + shows "\P\ c \R \<^bold>\ Q\" +using assms +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_conj_lift: + assumes x: "\P\ c \Q\" + assumes y: "\P'\ c \Q'\" + shows "\P \<^bold>\ P'\ c \Q \<^bold>\ Q'\" +apply (rule vcg_conj) + apply (rule vcg_pre[OF x], simp) +apply (rule vcg_pre[OF y], simp) +done + +lemma vcg_disj_lift: + assumes x: "\P\ c \Q\" + assumes y: "\P'\ c \Q'\" + shows "\P \<^bold>\ P'\ c \Q \<^bold>\ Q'\" +using assms +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_imp_lift: + assumes "\P'\ c \\<^bold>\ P\" + assumes "\Q'\ c \Q\" + shows "\P' \<^bold>\ Q'\ c \P \<^bold>\ Q\" +by (simp only: imp_conv_disj vcg_disj_lift[OF assms]) + +lemma vcg_ex_lift: + assumes "\x. \P x\ c \Q x\" + shows "\\s. \x. P x s\ c \\s. \x. Q x s\" +using assms +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_all_lift: + assumes "\x. \P x\ c \Q x\" + shows "\\s. \x. P x s\ c \\s. \x. Q x s\" +using assms +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_name_pre_state: + assumes "\s. P s \ \(=) s\ c \Q\" + shows "\P\ c \Q\" +using assms +by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+ + +lemma vcg_lift_comp: + assumes f: "\P. \\s. P (f s :: 'a :: type)\ c" + assumes P: "\x. \Q x\ c \P x\" + shows "\\s. Q (f s) s\ c \\s. P (f s) s\" +apply (rule vcg_name_pre_state) +apply (rename_tac s) +apply (rule vcg_pre) + apply (rule vcg_post_imp[rotated]) + apply (rule vcg_conj_lift) + apply (rule_tac x="f s" in P) + apply (rule_tac P="\fs. fs = f s" in f) + apply simp +apply simp +done + + +subsubsection\Cheap non-interference rules\ + +text\ + +These rules magically construct VCG lifting rules from the easier to +prove \eq_imp\ facts. We don't actually use these in the GC, +but we do derive @{const "fun_upd"} equations using the same +mechanism. Thanks to Thomas Sewell for the requisite syntax magic. + +As these \eq_imp\ facts do not usefully compose, we make the +definition asymmetric (i.e., \g\ does not get a bundle of +parameters). + +Note that these are effectively parametricity rules. + +\ + +definition eq_imp :: "('a \ 'b \ 'c) \ ('b \ 'e) \ bool" where + "eq_imp f g \ (\s s'. (\x. f x s = f x s') \ (g s = g s'))" + +lemma eq_impD: + "\ eq_imp f g; \x. f x s = f x s' \ \ g s = g s'" +by (simp add: eq_imp_def) + +lemma eq_imp_vcg: + assumes g: "eq_imp f g" + assumes f: "\x P. \P \ (f x)\ c" + shows "\P \ g\ c" +apply (rule vcg_name_pre_state) +apply (rename_tac s) +apply (rule vcg_pre) + apply (rule vcg_post_imp[rotated]) + apply (rule vcg_all_lift[where 'a='a]) + apply (rule_tac x=x and P="\fs. fs = f x s" in f[rule_format]) + apply simp + apply (frule eq_impD[where f=f, OF g]) + apply simp +apply simp +done + +lemma eq_imp_vcg_LST: + assumes g: "eq_imp f g" + assumes f: "\x P. \P \ (f x) \ LST\ c" + shows "\P \ g \ LST\ c" +apply (rule vcg_name_pre_state) +apply (rename_tac s) +apply (rule vcg_pre) + apply (rule vcg_post_imp[rotated]) + apply (rule vcg_all_lift[where 'a='a]) + apply (rule_tac x=x and P="\fs. fs = f x s\" in f[rule_format]) + apply simp + apply (frule eq_impD[where f=f, OF g]) + apply simp +apply simp +done + +lemma eq_imp_fun_upd: + assumes g: "eq_imp f g" + assumes f: "\x. f x (s(fld := val)) = f x s" + shows "g (s(fld := val)) = g s" +apply (rule eq_impD[OF g]) +apply (rule f) +done + +lemma curry_forall_eq: + "(\f. P f) = (\f. P (case_prod f))" +by (metis case_prod_curry) + +lemma pres_tuple_vcg: + "(\P. \P \ (\s. (f s, g s))\ c) + \ ((\P. \P \ f\ c) \ (\P. \P \ g\ c))" +apply (simp add: curry_forall_eq o_def) +apply safe + apply fast + apply fast +apply (rename_tac P) +apply (rule_tac f="f" and P="\fs s. P fs (g s)" in vcg_lift_comp; simp) +done + +lemma pres_tuple_vcg_LST: + "(\P. \P \ (\s. (f s, g s)) \ LST\ c) + \ ((\P. \P \ f \ LST\ c) \ (\P. \P \ g \ LST\ c))" +apply (simp add: curry_forall_eq o_def) +apply safe + apply fast + apply fast +apply (rename_tac P) +apply (rule_tac f="\s. f s\" and P="\fs s. P fs (g s)" for g in vcg_lift_comp; simp) +done + +no_notation valid_syn ("\_\/ _/ \_\") + +end + +(*<*) + +end +(*>*) diff --git a/thys/ConcurrentIMP/Infinite_Sequences.thy b/thys/ConcurrentIMP/Infinite_Sequences.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/Infinite_Sequences.thy @@ -0,0 +1,333 @@ +(*<*) +theory Infinite_Sequences +imports + CIMP_pred +begin + +(*>*) +section\ Infinite Sequences \label{sec:infinite_sequences}\ + +text\ + +Infinite sequences and some operations on them. + +We use the customary function-based representation. + +\ + +type_synonym 'a seq = "nat \ 'a" +type_synonym 'a seq_pred = "'a seq \ bool" + +definition suffix :: "'a seq \ nat \ 'a seq" (infixl "|\<^sub>s" 60) where + "\ |\<^sub>s i \ \j. \ (j + i)" + +primrec stake :: "nat \ 'a seq \ 'a list" where + "stake 0 \ = []" +| "stake (Suc n) \ = \ 0 # stake n (\ |\<^sub>s 1)" + +primrec shift :: "'a list \ 'a seq \ 'a seq" (infixr \@-\ 65) where + "shift [] \ = \" +| "shift (x # xs) \ = (\i. case i of 0 \ x | Suc i \ shift xs \ i)" + +(* FIXME misleading: this is \(i, i+j). Use a bundle for this notation. FIXME move *) +abbreviation interval_syn ("_'(_ \ _')" [69, 0, 0] 70) where (* FIXME priorities *) + "\(i \ j) \ stake j (\ |\<^sub>s i)" + +lemma suffix_eval: "(\ |\<^sub>s i) j = \ (j + i)" +unfolding suffix_def by simp + +lemma suffix_plus: "\ |\<^sub>s n |\<^sub>s m = \ |\<^sub>s (m + n)" +unfolding suffix_def by (simp add: add.assoc) + +lemma suffix_commute: "((\ |\<^sub>s n) |\<^sub>s m) = ((\ |\<^sub>s m) |\<^sub>s n)" +by (simp add: suffix_plus add.commute) + +lemma suffix_plus_com: "\ |\<^sub>s m |\<^sub>s n = \ |\<^sub>s (m + n)" +proof - + have "\ |\<^sub>s n |\<^sub>s m = \ |\<^sub>s (m + n)" by (rule suffix_plus) + then show "\ |\<^sub>s m |\<^sub>s n = \ |\<^sub>s (m + n)" by (simp add: suffix_commute) +qed + +lemma suffix_zero: "\ |\<^sub>s 0 = \" +unfolding suffix_def by simp + +lemma comp_suffix: "f \ \ |\<^sub>s i = (f \ \) |\<^sub>s i" +unfolding suffix_def comp_def by simp + +lemmas suffix_simps[simp] = + comp_suffix + suffix_eval + suffix_plus_com + suffix_zero + +lemma length_stake[simp]: "length (stake n s) = n" +by (induct n arbitrary: s) auto + +lemma shift_simps[simp]: + "(xs @- \) 0 = (if xs = [] then \ 0 else hd xs)" + "(xs @- \) |\<^sub>s Suc 0 = (if xs = [] then \ |\<^sub>s Suc 0 else tl xs @- \)" +by (induct xs) auto + +lemma stake_nil[simp]: + "stake i \ = [] \ i = 0" +by (cases i; clarsimp) + +lemma stake_shift: + "stake i (w @- \) = take i w @ stake (i - length w) \" +by (induct i arbitrary: w) (auto simp: neq_Nil_conv) + +lemma shift_snth_less[simp]: + assumes "i < length xs" + shows "(xs @- \) i = xs ! i" +using assms +proof(induct i arbitrary: xs) + case (Suc i xs) then show ?case by (cases xs) simp_all +qed (simp add: hd_conv_nth nth_tl) + +lemma shift_snth_ge[simp]: + assumes "i \ length xs" + shows "(xs @- \) i = \ (i - length xs)" +using assms +proof(induct i arbitrary: xs) + case (Suc i xs) then show ?case by (cases xs) simp_all +qed simp + +lemma shift_snth: + "(xs @- \) i = (if i < length xs then xs ! i else \ (i - length xs))" +by simp + +lemma suffix_shift: + "(xs @- \) |\<^sub>s i = drop i xs @- (\ |\<^sub>s i - length xs)" +proof(induct i arbitrary: xs) + case (Suc i xs) then show ?case by (cases xs) simp_all +qed simp + +lemma stake_nth[simp]: + assumes "i < j" + shows "stake j s ! i = s i" +using assms by (induct j arbitrary: s i) (simp_all add: nth_Cons') + +lemma stake_suffix_id: + "stake i \ @- (\ |\<^sub>s i) = \" +by (induct i) (simp_all add: fun_eq_iff shift_snth split: nat.splits) + +lemma id_stake_snth_suffix: + "\ = (stake i \ @ [\ i]) @- (\ |\<^sub>s Suc i)" +using stake_suffix_id +apply (metis Suc_diff_le append_Nil2 diff_is_0_eq length_stake lessI nat.simps(3) nat_le_linear shift_snth stake_nil stake_shift take_Suc_conv_app_nth) +done + +lemma stake_add[simp]: + "stake i \ @ stake j (\ |\<^sub>s i) = stake (i + j) \" +apply (induct i arbitrary: \) + apply simp +apply auto +apply (metis One_nat_def plus_1_eq_Suc suffix_plus_com) +done + +lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s" +proof (induct n arbitrary: u) + case (Suc n) then show ?case + apply clarsimp + apply (cases u) + apply auto + done +qed auto + +lemma stake_shift_stake_shift: + "stake i \ @- stake j (\ |\<^sub>s i) @- \ = stake (i + j) \ @- \" +apply (induct i arbitrary: \) + apply simp +apply auto +apply (metis One_nat_def plus_1_eq_Suc suffix_plus_com) +done + +lemma stake_suffix_drop: + "stake i (\ |\<^sub>s j) = drop j (stake (i + j) \)" +by (metis append_eq_conv_conj length_stake semiring_normalization_rules(24) stake_add) + +lemma stake_suffix: + assumes "i \ j" + shows "stake j \ @- u |\<^sub>s i = \(i \ j - i) @- u" +by (simp add: assms stake_suffix_drop suffix_shift) + + +subsection\Decomposing safety and liveness \label{sec:infinite_sequences-safety-liveness}\ + +text\ + +Famously properties on infinite sequences can be decomposed into +@{emph \safety\} and @{emph \liveness\} +properties @{cite "AlpernSchneider:1985" and "Schneider:1987"}. See +@{cite [cite_macro=citet] "Kindler:1994"} for an overview. + +\ + +definition safety :: "'a seq_pred \ bool" where + "safety P \ (\\. \P \ \ (\i. \\. \P (stake i \ @- \)))" + +lemma safety_def2: \ \Contraposition gives the customary prefix-closure definition\ + "safety P \ (\\. (\i. \\. P (stake i \ @- \)) \ P \)" +unfolding safety_def by blast + +definition liveness :: "'a seq_pred \ bool" where + "liveness P \ (\\. \\. P (\ @- \))" + +lemmas safetyI = iffD2[OF safety_def, rule_format] +lemmas safetyI2 = iffD2[OF safety_def2, rule_format] +lemmas livenessI = iffD2[OF liveness_def, rule_format] + +lemma safety_False: + shows "safety (\\. False)" +by (rule safetyI) simp + +lemma safety_True: + shows "safety (\\. True)" +by (rule safetyI) simp + +lemma safety_state_prop: + shows "safety (\\. P (\ 0))" +by (rule safetyI) auto + +lemma safety_invariant: + shows "safety (\\. \i. P (\ i))" +apply (rule safetyI) +apply clarsimp +apply (metis length_stake lessI shift_snth_less stake_nth) +done + +lemma safety_transition_relation: + shows "safety (\\. \i. (\ i, \ (i + 1)) \ R)" +apply (rule safetyI) +apply clarsimp +apply (metis (no_types, hide_lams) Suc_eq_plus1 add.left_neutral add_Suc_right add_diff_cancel_left' le_add1 list.sel(1) list.simps(3) shift_simps(1) stake.simps(2) stake_suffix suffix_def) +done + +lemma safety_conj: + assumes "safety P" + assumes "safety Q" + shows "safety (P \<^bold>\ Q)" +using assms unfolding safety_def by blast + +lemma safety_always_eventually[simplified]: + assumes "safety P" + assumes "\i. \j\i. \\. P (\(0 \ j) @- \)" + shows "P \" +using assms unfolding safety_def2 +apply - +apply (drule_tac x=\ in spec) +apply clarsimp +apply (drule_tac x=i in spec) +apply clarsimp +apply (rule_tac x="(stake j \ @- \) |\<^sub>s i" in exI) +apply (simp add: stake_shift_stake_shift stake_suffix) +done + +lemma safety_disj: + assumes "safety P" + assumes "safety Q" + shows "safety (P \<^bold>\ Q)" +unfolding safety_def2 using assms +by (metis safety_always_eventually add_diff_cancel_right' diff_le_self le_add_same_cancel2) + +text\ + +The decomposition is given by a form of closure. + +\ + +definition M\<^sub>p :: "'a seq_pred \ 'a seq_pred" where + "M\<^sub>p P = (\\. \i. \\. P (stake i \ @- \))" + +definition Safe :: "'a seq_pred \ 'a seq_pred" where + "Safe P = (P \<^bold>\ M\<^sub>p P)" + +definition Live :: "'a seq_pred \ 'a seq_pred" where + "Live P = (P \<^bold>\ \<^bold>\M\<^sub>p P)" + +lemma decomp: + "P = (Safe P \<^bold>\ Live P)" +unfolding Safe_def Live_def by blast + +lemma safe: + "safety (Safe P)" +unfolding Safe_def safety_def M\<^sub>p_def +apply clarsimp +apply (simp add: stake_shift) +apply (rule_tac x=i in exI) +apply clarsimp +apply (rule_tac x=i in exI) +apply clarsimp +done + +lemma live: + "liveness (Live P)" +proof(rule livenessI) + fix \ + have "(\\. P (\ @- \)) \ \(\\. P (\ @- \))" by blast + also have "?this \ (\\. P (\ @- \) \ (\\. \P (\ @- \)))" by blast + also have "\ \ (\\. P (\ @- \) \ (\i. i = length \ \ (\\. \P (stake i (\ @- \) @- \))))" by (simp add: stake_shift) + also have "\ \ (\\. P (\ @- \) \ (\i. (\\. \P (stake i (\ @- \) @- \))))" by blast + finally have "\\. P (\ @- \) \ (\i. \\. \ P (stake i (\ @- \) @- \))" . + then show "\\. Live P (\ @- \)" unfolding Live_def M\<^sub>p_def by simp +qed + +text\ + +@{cite "Sistla:1994"} proceeds to give a topological analysis of fairness. An \<^emph>\absolute\ +liveness property is a liveness property whose complement is stable. + +\ + +definition absolute_liveness :: "'a seq_pred \ bool" where \ \ closed under prepending any finite sequence \ + "absolute_liveness P \ (\\. P \) \ (\\ \. P \ \ P (\ @- \))" + +definition stable :: "'a seq_pred \ bool" where \ \ closed under suffixes \ + "stable P \ (\\. P \) \ (\\ i. P \ \ P (\ |\<^sub>s i))" + +lemma absolute_liveness_liveness: + assumes "absolute_liveness P" + shows "liveness P" +using assms unfolding absolute_liveness_def liveness_def by blast + +lemma stable_absolute_liveness: + assumes "P \" + assumes "\P \'" \\ extra hypothesis \ + shows "stable P \ absolute_liveness (\<^bold>\ P)" +using assms unfolding stable_def absolute_liveness_def +apply auto + apply (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) suffix_shift suffix_zero) +apply (metis stake_suffix_id) +done + +(* +text\ + +Fairness ala Sistla. Unmotivated. + +FIXME safety properties are insensitive to fairness. +FIXME typically we prove \sys \ safety\. The result below doesn't appear strong enough. +FIXME observe fairness is a special liveness property. + +\ +*) + +definition fairness :: "'a seq_pred \ bool" where + "fairness P \ stable P \ absolute_liveness P" + +lemma fairness_safety: + assumes "safety P" + assumes "fairness F" + shows "(\\. F \ \ P \) \ (\\. P \)" +apply rule +using assms +apply clarsimp +unfolding safety_def fairness_def stable_def absolute_liveness_def +apply clarsimp +apply blast+ +done + +(*<*) + +end +(*>*) diff --git a/thys/ConcurrentIMP/LTL.thy b/thys/ConcurrentIMP/LTL.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/LTL.thy @@ -0,0 +1,828 @@ +(*<*) +theory LTL +imports + CIMP_pred + Infinite_Sequences +begin + +(*>*) +section\ Linear Temporal Logic \label{sec:ltl}\ + +text\ + +To talk about liveness we need to consider infinitary behaviour on +sequences. Traditionally future-time linear temporal logic (LTL) is used to do +this @{cite "MannaPnueli:1991" and "OwickiLamport:1982"}. + +The following is a straightforward shallow embedding of the +now-traditional anchored semantics of LTL @{cite "MannaPnueli:1988"}. Some of it is adapted +from the sophisticated TLA development in the AFP due to @{cite [cite_macro=citet] "TLA-AFP"}. + +Unlike @{cite [cite_macro=citet] "Lamport:2002"}, include the +next operator, which is convenient for stating rules. Sometimes it allows us to +ignore the system, i.e. to state rules as temporally valid +(LTL-valid) rather than just temporally program valid (LTL-cimp-), in Jackson's terminology. + +\ + +definition state_prop :: "('a \ bool) \ 'a seq_pred" ("\_\") where + "\P\ = (\\. P (\ 0))" + +definition "next" :: "'a seq_pred \ 'a seq_pred" ("\_" [80] 80) where + "(\P) = (\\. P (\ |\<^sub>s 1))" + +definition always :: "'a seq_pred \ 'a seq_pred" ("\_" [80] 80) where + "(\P) = (\\. \i. P (\ |\<^sub>s i))" + +definition until :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" (infixr "\" 30) where (* FIXME priority, binds tighter than \<^bold>\ *) + "(P \ Q) = (\\. \i. Q (\ |\<^sub>s i) \ (\k |\<^sub>s k)))" + +definition eventually :: "'a seq_pred \ 'a seq_pred" ("\_" [80] 80) where (* FIXME priority, consider making an abbreviation *) + "(\P) = (\True\ \ P)" + +definition release :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" (infixr "\" 30) where (* FIXME priority, dual of Until *) + "(P \ Q) = (\<^bold>\(\<^bold>\P \ \<^bold>\Q))" + +definition unless :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" (infixr "\" 30) where (* FIXME priority, aka weak until *) + "(P \ Q) = ((P \ Q) \<^bold>\ \P)" + +abbreviation (input) + pred_always_imp_syn :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" (infixr "\<^bold>\" 25) where + "P \<^bold>\ Q \ \(P \<^bold>\ Q)" + +lemmas defs = + state_prop_def + always_def + eventually_def + next_def + release_def + unless_def + until_def + +lemma suffix_state_prop[simp]: + shows "\P\ (\ |\<^sub>s i) = P (\ i)" +unfolding defs by simp + +lemma alwaysI[intro]: + assumes "\i. P (\ |\<^sub>s i)" + shows "(\P) \" +unfolding defs using assms by blast + +lemma alwaysD: + assumes "(\P) \" + shows "P (\ |\<^sub>s i)" +using assms unfolding defs by blast + +lemma alwaysE: "\(\P) \; P (\ |\<^sub>s i) \ Q\ \ Q" +unfolding defs by blast + +lemma always_induct: + assumes "P \" + assumes "(\(P \<^bold>\ \P)) \" + shows "(\P) \" +proof(rule alwaysI) + fix i from assms show "P (\ |\<^sub>s i)" + unfolding defs by (induct i) simp_all +qed + +lemma seq_comp: + fixes \ :: "'a seq" + fixes P :: "'b seq_pred" + fixes f :: "'a \ 'b" + shows + "(\P) (f \ \) \ (\(\\. P (f \ \))) \" + "(\P) (f \ \) \ (\(\\. P (f \ \))) \" + "(P \ Q) (f \ \) \ ((\\. P (f \ \)) \ (\\. Q (f \ \))) \" + "(P \ Q) (f \ \) \ ((\\. P (f \ \)) \ (\\. Q (f \ \))) \" +unfolding defs by simp_all + +lemma nextI[intro]: + assumes "P (\ |\<^sub>s Suc 0)" + shows "(\P) \" +using assms unfolding defs by simp + +lemma untilI[intro]: + assumes "Q (\ |\<^sub>s i)" + assumes "\k |\<^sub>s k)" + shows "(P \ Q) \" +unfolding defs using assms by blast + +lemma untilE: + assumes "(P \ Q) \" + obtains i where "Q (\ |\<^sub>s i)" and "\k |\<^sub>s k)" +using assms unfolding until_def by blast + +lemma eventuallyI[intro]: + assumes "P (\ |\<^sub>s i)" + shows "(\P) \" +unfolding eventually_def using assms by blast + +lemma eventuallyE[elim]: + assumes "(\P) \" + obtains i where "P (\ |\<^sub>s i)" +using assms unfolding defs by (blast elim: untilE) + +lemma unless_alwaysI: + assumes "(\ P) \" + shows "(P \ Q) \" +using assms unfolding defs by blast + +lemma unless_untilI: + assumes "Q (\ |\<^sub>s j)" + assumes "\i. i < j \ P (\ |\<^sub>s i)" + shows "(P \ Q) \" +unfolding defs using assms by blast + +lemma always_imp_refl[iff]: + shows "(P \<^bold>\ P) \" +unfolding defs by blast + +lemma always_imp_trans: + assumes "(P \<^bold>\ Q) \" + assumes "(Q \<^bold>\ R) \" + shows "(P \<^bold>\ R) \" +using assms unfolding defs by blast + +lemma always_imp_mp: + assumes "(P \<^bold>\ Q) \" + assumes "P \" + shows "Q \" +using assms unfolding defs by (metis suffix_zero) + +lemma always_imp_mp_suffix: + assumes "(P \<^bold>\ Q) \" + assumes "P (\ |\<^sub>s i)" + shows "Q (\ |\<^sub>s i)" +using assms unfolding defs by metis + +text\ + +Some basic facts and equivalences, mostly sanity. + +\ + +lemma necessitation: + "(\s. P s) \ (\P) \" + "(\s. P s) \ (\P) \" + "(\s. P s) \ (P \ Q) \" + "(\s. Q s) \ (P \ Q) \" +unfolding defs by auto + +lemma cong: + "(\s. P s = P' s) \ \P\ = \P'\" + "(\\. P \ = P' \) \ (\P) = (\P')" + "(\\. P \ = P' \) \ (\P) = (\P')" + "(\\. P \ = P' \) \ (\P) = (\P')" + "\\\. P \ = P' \; \\. Q \ = Q' \\ \ (P \ Q) = (P' \ Q')" + "\\\. P \ = P' \; \\. Q \ = Q' \\ \ (P \ Q) = (P' \ Q')" +unfolding defs by auto + +lemma norm[simp]: + "\\False\\ = \False\" + "\\True\\ = \True\" + "(\<^bold>\\p\) = \\<^bold>\p\" + "(\p\ \<^bold>\ \q\) = \p \<^bold>\ q\" + "(\p\ \<^bold>\ \q\) = \p \<^bold>\ q\" + "(\p\ \<^bold>\ \q\) = \p \<^bold>\ q\" + "(\p\ \ \ \q\ \) = \p \<^bold>\ q\ \" + "(\p\ \ \ \q\ \) = \p \<^bold>\ q\ \" + "(\p\ \ \ \q\ \) = \p \<^bold>\ q\ \" + + "(\\False\) = \False\" + "(\\True\) = \True\" + + "(\\False\) = \False\" + "(\\True\) = \True\" + "(\<^bold>\\ P) \ = (\ (\<^bold>\ P)) \" + "(\\ P) = (\ P)" + + "(\\False\) = \False\" + "(\\True\) = \True\" + "(\<^bold>\\ P) = (\ (\<^bold>\ P))" + "(\\ P) = (\ P)" + + "(P \ \False\) = (\ P)" + + "(\<^bold>\(P \ Q)) \ = (\<^bold>\P \ \<^bold>\Q) \" + "(\False\ \ P) = P" + "(P \ \False\) = \False\" + "(P \ \True\) = \True\" + "(\True\ \ P) = (\ P)" + "(P \ (P \ Q)) = (P \ Q)" + + "(\<^bold>\(P \ Q)) \ = (\<^bold>\P \ \<^bold>\Q) \" + "(\False\ \ P) = (\P)" + "(P \ \False\) = \False\" + "(\True\ \ P) = P" + "(P \ \True\) = \True\" +(* + "(P \ (P \ Q)) \ = (P \ Q) \" FIXME for Release +*) +unfolding defs +apply (auto simp: fun_eq_iff) +apply (metis suffix_plus suffix_zero) +apply (metis suffix_plus suffix_zero) + apply fastforce + apply force +apply (metis add.commute add_diff_inverse_nat less_diff_conv2 not_le) +apply (metis add.right_neutral not_less0) + apply force + apply fastforce +done + +lemma always_conj_distrib: "(\(P \<^bold>\ Q)) = (\P \<^bold>\ \Q)" +unfolding defs by auto + +lemma eventually_disj_distrib: "(\(P \<^bold>\ Q)) = (\P \<^bold>\ \Q)" +unfolding defs by auto + +lemma always_eventually[elim!]: + assumes "(\P) \" + shows "(\P) \" +using assms unfolding defs by auto + +lemma eventually_imp_conv_disj: "(\(P \<^bold>\ Q)) = (\(\<^bold>\P) \<^bold>\ \Q)" +unfolding defs by auto + +lemma eventually_imp_distrib: + "(\(P \<^bold>\ Q)) = (\P \<^bold>\ \Q)" +unfolding defs by auto + +lemma unfold: + "(\ P) \ = (P \<^bold>\ \\P) \" + "(\ P) \ = (P \<^bold>\ \\P) \" + "(P \ Q) \ = (Q \<^bold>\ (P \<^bold>\ \(P \ Q))) \" + "(P \ Q) \ = (Q \<^bold>\ (P \<^bold>\ \(P \ Q))) \" + "(P \ Q) \ = (Q \<^bold>\ (P \<^bold>\ \(P \ Q))) \" +unfolding defs +apply - +apply (metis (full_types) add.commute add_diff_inverse_nat less_one suffix_plus suffix_zero) +apply (metis (full_types) One_nat_def add.right_neutral add_Suc_right lessI less_Suc_eq_0_disj suffix_plus suffix_zero) + +apply auto + apply fastforce + apply (metis gr0_conv_Suc nat_neq_iff not_less_eq suffix_zero) + apply (metis suffix_zero) + apply force + using less_Suc_eq_0_disj apply fastforce + apply (metis gr0_conv_Suc nat_neq_iff not_less0 suffix_zero) + + apply fastforce + apply (case_tac i; auto) + apply force + using less_Suc_eq_0_disj apply force + + apply force + using less_Suc_eq_0_disj apply fastforce + apply fastforce + apply (case_tac i; auto) +done + +lemma mono: + "\(\P) \; \\. P \ \ P' \\ \ (\P') \" + "\(\P) \; \\. P \ \ P' \\ \ (\P') \" + "\(P \ Q) \; \\. P \ \ P' \; \\. Q \ \ Q' \\ \ (P' \ Q') \" + "\(P \ Q) \; \\. P \ \ P' \; \\. Q \ \ Q' \\ \ (P' \ Q') \" +unfolding defs by force+ + +lemma always_imp_mono: + "\(\P) \; (P \<^bold>\ P') \\ \ (\P') \" + "\(\P) \; (P \<^bold>\ P') \\ \ (\P') \" + "\(P \ Q) \; (P \<^bold>\ P') \; (Q \<^bold>\ Q') \\ \ (P' \ Q') \" + "\(P \ Q) \; (P \<^bold>\ P') \; (Q \<^bold>\ Q') \\ \ (P' \ Q') \" +unfolding defs by force+ + +lemma next_conj_distrib: + "(\(P \<^bold>\ Q)) = (\P \<^bold>\ \Q)" +unfolding defs by auto + +lemma next_disj_distrib: + "(\(P \<^bold>\ Q)) = (\P \<^bold>\ \Q)" +unfolding defs by auto + +lemma until_next_distrib: + "(\(P \ Q)) = (\P \ \Q)" +unfolding defs by (auto simp: fun_eq_iff) + +lemma until_imp_eventually: + "((P \ Q) \<^bold>\ \Q) \" +unfolding defs by auto + +lemma until_until_disj: + assumes "(P \ Q \ R) \" + shows "((P \<^bold>\ Q) \ R) \" +using assms unfolding defs +apply clarsimp +apply (metis (full_types) add_diff_inverse_nat nat_add_left_cancel_less) +done + +lemma unless_unless_disj: + assumes "(P \ Q \ R) \" + shows "((P \<^bold>\ Q) \ R) \" +using assms unfolding defs +apply auto + apply (metis add.commute add_diff_inverse_nat leI less_diff_conv2) +apply (metis add_diff_inverse_nat) +done + +lemma until_conj_distrib: + "((P \<^bold>\ Q) \ R) = ((P \ R) \<^bold>\ (Q \ R))" +unfolding defs +apply (auto simp: fun_eq_iff) +apply (metis dual_order.strict_trans nat_neq_iff) +done + +lemma until_disj_distrib: + "(P \ (Q \<^bold>\ R)) = ((P \ Q) \<^bold>\ (P \ R))" +unfolding defs by (auto simp: fun_eq_iff) + +lemma eventually_until: + "(\P) = (\<^bold>\P \ P)" +unfolding defs +apply (auto simp: fun_eq_iff) +apply (case_tac "P (x |\<^sub>s 0)") + apply blast +apply (drule (1) ex_least_nat_less) +apply (metis le_simps(2)) +done + +lemma eventually_until_eventually: + "(\(P \ Q)) = (\Q)" +unfolding defs by force + +lemma eventually_unless_until: + "((P \ Q) \<^bold>\ \Q) = (P \ Q)" +unfolding defs by force + +lemma eventually_always_imp_always_eventually: + assumes "(\\P) \" + shows "(\\P) \" +using assms unfolding defs by (metis suffix_commute) + +lemma eventually_always_next_stable: + assumes "(\P) \" + assumes "(P \<^bold>\ \P) \" + shows "(\\P) \" +using assms by (metis (no_types) eventuallyI alwaysD always_induct eventuallyE norm(15)) + +lemma next_stable_imp_eventually_always: + assumes "(P \<^bold>\ \P) \" + shows "(\P \<^bold>\ \\P) \" +using assms eventually_always_next_stable by blast + +lemma always_eventually_always: + "\\\P = \\P" +unfolding defs by (clarsimp simp: fun_eq_iff) (metis add.left_commute semiring_normalization_rules(25)) + +(* FIXME define "stable", develop more rules for it *) +lemma stable_unless: + assumes "(P \<^bold>\ \(P \<^bold>\ Q)) \" + shows "(P \<^bold>\ (P \ Q)) \" +using assms unfolding defs +apply - +apply (rule ccontr) +apply clarsimp +apply (drule (1) ex_least_nat_less[where P="\j. \P (\ |\<^sub>s i + j)" for i, simplified]) +apply clarsimp +apply (metis add_Suc_right le_less less_Suc_eq) +done + +lemma unless_induct: \\ Rule \texttt{WAIT} from @{cite [cite_macro=citet] \Fig~3.3\ "MannaPnueli:1995"}\ + assumes I: "(I \<^bold>\ \(I \<^bold>\ R)) \" + assumes P: "(P \<^bold>\ I \<^bold>\ R) \" + assumes Q: "(I \<^bold>\ Q) \" + shows "(P \<^bold>\ Q \ R) \" +apply (intro alwaysI impI) +apply (erule impE[OF alwaysD[OF P]]) +apply (erule disjE) + apply (rule always_imp_mono(4)[where P=I and Q=R]) + apply (erule mp[OF alwaysD[OF stable_unless[OF I]]]) + apply (simp add: Q alwaysD) + apply blast +apply (simp add: unfold) +done + + +subsection\ Leads-to and leads-to-via \label{sec:leads-to} \ + +text\ + +Most of our assertions will be of the form @{term "A \<^bold>\ \C"} (pronounced ``\A\ leads to \C\'') +or @{term "A \<^bold>\ B \ C"} (``\A\ leads to \C\ via \B\''). + +Most of these rules are due to @{cite [cite_macro=citet] +"Jackson:1998"} who used leads-to-via in a sequential setting. Others +are due to @{cite [cite_macro=citet] "MannaPnueli:1991"}. + +The leads-to-via connective is similar to the ``ensures'' modality of @{cite [cite_macro=citet] \\S3.4.4\ "ChandyMisra:1989"}. + +\ + +abbreviation (input) + leads_to :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" (infixr "\<^bold>\" 25) where (* FIXME priority *) + "P \<^bold>\ Q \ P \<^bold>\ \Q" + +lemma leads_to_refl: + shows "(P \<^bold>\ P) \" +by (metis (no_types, lifting) necessitation(1) unfold(2)) + +lemma leads_to_trans: + assumes "(P \<^bold>\ Q) \" + assumes "(Q \<^bold>\ R) \" + shows "(P \<^bold>\ R) \" +using assms unfolding defs by clarsimp (metis semiring_normalization_rules(25)) + +lemma leads_to_eventuallyE: + assumes "(P \<^bold>\ Q) \" + assumes "(\P) \" + shows "(\Q) \" +using assms unfolding defs by auto + +lemma leads_to_mono: + assumes "(P' \<^bold>\ P) \" + assumes "(Q \<^bold>\ Q') \" + assumes "(P \<^bold>\ Q) \" + shows "(P' \<^bold>\ Q') \" +using assms unfolding defs by clarsimp blast + +lemma leads_to_eventually: + shows "(P \<^bold>\ Q \<^bold>\ \P \<^bold>\ \Q) \" +by (metis (no_types, lifting) alwaysI unfold(2)) + +lemma leads_to_disj: + assumes "(P \<^bold>\ R) \" + assumes "(Q \<^bold>\ R) \" + shows "((P \<^bold>\ Q) \<^bold>\ R) \" +using assms unfolding defs by simp + +lemma leads_to_leads_to_viaE: + shows "((P \<^bold>\ P \ Q) \<^bold>\ P \<^bold>\ Q) \" +unfolding defs by clarsimp blast + +lemma leads_to_via_concl_weaken: + assumes "(R \<^bold>\ R') \" + assumes "(P \<^bold>\ Q \ R) \" + shows "(P \<^bold>\ Q \ R') \" +using assms unfolding LTL.defs by force + +lemma leads_to_via_trans: + assumes "(A \<^bold>\ B \ C) \" + assumes "(C \<^bold>\ D \ E) \" + shows "(A \<^bold>\ (B \<^bold>\ D) \ E) \" +proof(rule alwaysI, rule impI) + fix i assume "A (\ |\<^sub>s i)" with assms show "((B \<^bold>\ D) \ E) (\ |\<^sub>s i)" + apply - + apply (erule alwaysE[where i=i]) + apply clarsimp + apply (erule untilE) + apply clarsimp (* suffix *) + apply (drule (1) always_imp_mp_suffix) + apply (erule untilE) + apply clarsimp (* suffix *) + apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps) + apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *) + done +qed + +lemma leads_to_via_disj: \ \ useful for case distinctions \ + assumes "(P \<^bold>\ Q \ R) \" + assumes "(P' \<^bold>\ Q' \ R) \" + shows "(P \<^bold>\ P' \<^bold>\ (Q \<^bold>\ Q') \ R) \" +using assms unfolding defs by (auto 10 0) + +lemma leads_to_via_disj': \ \ more like a chaining rule \ + assumes "(A \<^bold>\ B \ C) \" + assumes "(C \<^bold>\ D \ E) \" + shows "(A \<^bold>\ C \<^bold>\ (B \<^bold>\ D) \ E) \" +proof(rule alwaysI, rule impI, erule disjE) + fix i assume "A (\ |\<^sub>s i)" with assms show "((B \<^bold>\ D) \ E) (\ |\<^sub>s i)" + apply - + apply (erule alwaysE[where i=i]) + apply clarsimp + apply (erule untilE) + apply clarsimp (* suffix *) + apply (drule (1) always_imp_mp_suffix) + apply (erule untilE) + apply clarsimp (* suffix *) + apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps) + apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *) + done +next + fix i assume "C (\ |\<^sub>s i)" with assms(2) show "((B \<^bold>\ D) \ E) (\ |\<^sub>s i)" + apply - + apply (erule alwaysE[where i=i]) + apply (simp add: mono) + done +qed + +lemma leads_to_via_stable_augmentation: + assumes stable: "(P \<^bold>\ Q \<^bold>\ \Q) \" + assumes U: "(A \<^bold>\ P \ C) \" + shows "((A \<^bold>\ Q) \<^bold>\ P \ (C \<^bold>\ Q)) \" +proof(intro alwaysI impI, elim conjE) + fix i assume AP: "A (\ |\<^sub>s i)" "Q (\ |\<^sub>s i)" + have "Q (\ |\<^sub>s (j + i))" if "Q (\ |\<^sub>s i)" and "\k |\<^sub>s (k + i))" for j + using that stable by (induct j; force simp: defs) + with U AP show "(P \ (\\. C \ \ Q \)) (\ |\<^sub>s i)" + unfolding defs by clarsimp (metis (full_types) add.commute) +qed + +lemma leads_to_via_wf: + assumes "wf R" + assumes indhyp: "\t. (A \<^bold>\ \\ \<^bold>= \t\\ \<^bold>\ B \ (A \<^bold>\ \\ \<^bold>\ \t\ \<^bold>\ \R\\ \<^bold>\ C)) \" + shows "(A \<^bold>\ B \ C) \" +proof(intro alwaysI impI) + fix i assume "A (\ |\<^sub>s i)" with \wf R\ show "(B \ C) (\ |\<^sub>s i)" + proof(induct "\ (\ i)" arbitrary: i) + case (less i) with indhyp[where t="\ (\ i)"] show ?case + apply - + apply (drule alwaysD[where i=i]) + apply clarsimp + apply (erule untilE) + apply (rename_tac j) + apply (erule disjE; clarsimp) + apply (drule_tac x="i + j" in meta_spec; clarsimp) + apply (erule untilE; clarsimp) + apply (rename_tac j k) + apply (rule_tac i="j + k" in untilI) + apply (simp add: add.assoc) + apply clarsimp + apply (metis add.assoc add.commute add_diff_inverse_nat less_diff_conv2 not_le) + apply auto + done + qed +qed + +text\ + +The well-founded response rule due to @{cite [cite_macro=citet] \Fig~1.23: \texttt{WELL} (well-founded response)\"MannaPnueli:2010"}, +generalised to an arbitrary set of assertions and sequence predicates. +\<^item> \W1\ generalised to be contingent. +\<^item> \W2\ is a well-founded set of assertions that by \W1\ includes \P\ + +\ + +(* FIXME: Does \Is\ need to be consistent? *) +lemma leads_to_wf: + fixes Is :: "('a seq_pred \ ('a \ 'b)) set" + assumes "wf (R :: 'b rel)" + assumes W1: "(\(\<^bold>\\. \\\\fst ` Is\\ \<^bold>\ (P \<^bold>\ \))) \" + assumes W2: "\(\, \)\Is. \(\', \')\insert (Q, \0) Is. \t. (\ \<^bold>\ \\ \<^bold>= \t\\ \<^bold>\ \' \<^bold>\ \\' \<^bold>\ \t\ \<^bold>\ \R\\) \" + shows "(P \<^bold>\ Q) \" +proof - + have "(\ \<^bold>\ \\ \<^bold>= \t\\ \<^bold>\ Q) \" if "(\, \) \ Is" for \ \ t + using \wf R\ that W2 + apply (induct t arbitrary: \ \) + unfolding LTL.defs split_def + apply clarsimp + apply (metis (no_types, hide_lams) ab_semigroup_add_class.add_ac(1) fst_eqD snd_conv surjective_pairing) + done + with W1 show ?thesis + apply - + apply (rule alwaysI) + apply clarsimp + apply (erule_tac i=i in alwaysE) + apply clarsimp + using alwaysD suffix_state_prop apply blast + done +qed + + +subsection\Fairness\ + +text\ + +A few renderings of weak fairness. @{cite [cite_macro=citet] "vanGlabbeekHofner:2019"} call this +"response to insistence" as a generalisation of weak fairness. + +\ + +definition weakly_fair :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" where + "weakly_fair enabled taken = (\enabled \<^bold>\ \taken)" + +lemma weakly_fair_def2: + shows "weakly_fair enabled taken = \(\<^bold>\\(enabled \<^bold>\ \<^bold>\taken))" +unfolding weakly_fair_def by (metis (full_types) always_conj_distrib norm(18)) + +lemma weakly_fair_def3: + shows "weakly_fair enabled taken = (\\enabled \<^bold>\ \\taken)" +unfolding weakly_fair_def2 +apply (clarsimp simp: fun_eq_iff) + +unfolding defs (* True, but can we get there deductively? *) +apply auto +apply (metis (full_types) add.left_commute semiring_normalization_rules(25)) +done + +lemma weakly_fair_def4: + shows "weakly_fair enabled taken = \\(enabled \<^bold>\ taken)" +using weakly_fair_def2 by force + +lemma mp_weakly_fair: + assumes "weakly_fair enabled taken \" + assumes "(\enabled) \" + shows "(\taken) \" +using assms unfolding weakly_fair_def using always_imp_mp by blast + +lemma always_weakly_fair: + shows "\(weakly_fair enabled taken) = weakly_fair enabled taken" +unfolding weakly_fair_def by simp + +lemma eventually_weakly_fair: + shows "\(weakly_fair enabled taken) = weakly_fair enabled taken" +unfolding weakly_fair_def2 by (simp add: always_eventually_always) + +lemma weakly_fair_weaken: + assumes "(enabled' \<^bold>\ enabled) \" + assumes "(taken \<^bold>\ taken') \" + shows "(weakly_fair enabled taken \<^bold>\ weakly_fair enabled' taken') \" +using assms unfolding weakly_fair_def defs by simp blast + +lemma weakly_fair_unless_until: + shows "(weakly_fair enabled taken \<^bold>\ (enabled \<^bold>\ enabled \ taken)) = (enabled \<^bold>\ enabled \ taken)" +unfolding defs weakly_fair_def +apply (auto simp: fun_eq_iff) +apply (metis add.right_neutral) +done + +lemma stable_leads_to_eventually: + assumes "(enabled \<^bold>\ \(enabled \<^bold>\ taken)) \" + shows "(enabled \<^bold>\ (\enabled \<^bold>\ \taken)) \" +using assms unfolding defs +apply - +apply (rule ccontr) +apply clarsimp +apply (drule (1) ex_least_nat_less[where P="\j. \ enabled (\ |\<^sub>s i + j)" for i, simplified]) +apply clarsimp +apply (metis add_Suc_right leI less_irrefl_nat) +done + +lemma weakly_fair_stable_leads_to: + assumes "(weakly_fair enabled taken) \" + assumes "(enabled \<^bold>\ \(enabled \<^bold>\ taken)) \" + shows "(enabled \<^bold>\ taken) \" +using stable_leads_to_eventually[OF assms(2)] assms(1) unfolding defs weakly_fair_def +by (auto simp: fun_eq_iff) + +lemma weakly_fair_stable_leads_to_via: + assumes "(weakly_fair enabled taken) \" + assumes "(enabled \<^bold>\ \(enabled \<^bold>\ taken)) \" + shows "(enabled \<^bold>\ enabled \ taken) \" +using stable_unless[OF assms(2)] assms(1) by (metis (mono_tags) weakly_fair_unless_until) + +text\ + +Similarly for strong fairness. @{cite [cite_macro=citet] "vanGlabbeekHofner:2019"} call this +"response to persistence" as a generalisation of strong fairness. + +\ + +definition strongly_fair :: "'a seq_pred \ 'a seq_pred \ 'a seq_pred" where + "strongly_fair enabled taken = (\\enabled \<^bold>\ \taken)" + +lemma strongly_fair_def2: + "strongly_fair enabled taken = \(\<^bold>\\(\enabled \<^bold>\ \<^bold>\taken))" +unfolding strongly_fair_def by (metis weakly_fair_def weakly_fair_def2) + +lemma strongly_fair_def3: + "strongly_fair enabled taken = (\\enabled \<^bold>\ \\taken)" +unfolding strongly_fair_def2 by (metis (full_types) always_eventually_always weakly_fair_def2 weakly_fair_def3) + +lemma always_strongly_fair: + "\(strongly_fair enabled taken) = strongly_fair enabled taken" +unfolding strongly_fair_def by simp + +lemma eventually_strongly_fair: + "\(strongly_fair enabled taken) = strongly_fair enabled taken" +unfolding strongly_fair_def2 by (simp add: always_eventually_always) + +lemma strongly_fair_disj_distrib: \ \not true for \weakly_fair\\ + "strongly_fair (enabled1 \<^bold>\ enabled2) taken = (strongly_fair enabled1 taken \<^bold>\ strongly_fair enabled2 taken)" +unfolding strongly_fair_def defs +apply (auto simp: fun_eq_iff) + apply blast + apply blast + apply (metis (full_types) semiring_normalization_rules(25)) +done + +lemma strongly_fair_imp_weakly_fair: + assumes "strongly_fair enabled taken \" + shows "weakly_fair enabled taken \" +using assms unfolding strongly_fair_def3 weakly_fair_def3 by (simp add: eventually_always_imp_always_eventually) + +lemma always_enabled_weakly_fair_strongly_fair: + assumes "(\enabled) \" + shows "weakly_fair enabled taken \ = strongly_fair enabled taken \" +using assms by (metis strongly_fair_def3 strongly_fair_imp_weakly_fair unfold(2) weakly_fair_def3) + + +subsection\Safety and liveness \label{sec:ltl-safety-liveness}\ + +text\ + +@{cite [cite_macro=citet] "Sistla:1994"} shows some characterisations +of LTL formulas in terms of safety and liveness. Note his @{term +"(\)"} is actually @{term "(\)"}. + +See also @{cite [cite_macro=citet] "ChangMannaPnueli:1992"}. + +\ + +lemma safety_state_prop: + shows "safety \P\" +unfolding defs by (rule safety_state_prop) + +lemma safety_Next: + assumes "safety P" + shows "safety (\P)" +using assms unfolding defs safety_def +apply clarsimp +apply (metis (mono_tags) One_nat_def list.sel(3) nat.simps(3) stake.simps(2)) +done + +lemma safety_unless: + assumes "safety P" + assumes "safety Q" + shows "safety (P \ Q)" +proof(rule safetyI2) + fix \ assume X: "\\. (P \ Q) (stake i \ @- \)" for i + then show "(P \ Q) \" + proof(cases "\i j. \\. P (\(i \ j) @- \)") + case True + with \safety P\ have "\i. P (\ |\<^sub>s i)" unfolding safety_def2 by blast + then show ?thesis by (blast intro: unless_alwaysI) + next + case False + then obtain k k' where "\\. \ P (\(k \ k') @- \)" by clarsimp + then have "\i u. k + k' \ i \ \P ((stake i \ @- u) |\<^sub>s k)" + by (metis add.commute diff_add stake_shift_stake_shift stake_suffix_drop suffix_shift) + then have "\i u. k + k' \ i \ (P \ Q) (stake i \ @- u) \ (\m\k. Q ((stake i \ @- u) |\<^sub>s m) \ (\p @- u) |\<^sub>s p)))" + unfolding defs using leI by blast + then have "\i u. k + k' \ i \ (P \ Q) (stake i \ @- u) \ (\m\k. Q (\(m \ i - m) @- u) \ (\p(p \ i - p) @- u)))" + by (metis stake_suffix add_leE nat_less_le order_trans) + then have "\i. \n\i. \m\k. \u. Q (\(m \ n - m) @- u) \ (\p(p \ n - p) @- u))" + using X by (metis add.commute le_add1) + then have "\m\k. \i. \n\i. \u. Q (\(m \ n - m) @- u) \ (\p(p \ n - p) @- u))" + by (simp add: always_eventually_pigeonhole) + with \safety P\ \safety Q\ show "(P \ Q) \" + unfolding defs by (metis Nat.le_diff_conv2 add_leE safety_always_eventually) + qed +qed + +lemma safety_always: + assumes "safety P" + shows "safety (\P)" +using assms by (metis norm(20) safety_def safety_unless) + +lemma absolute_liveness_eventually: + shows "absolute_liveness P \ (\\. P \) \ P = \P" +unfolding absolute_liveness_def defs +by (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) stake_suffix_id suffix_shift suffix_zero) + +lemma stable_always: + shows "stable P \ (\\. P \) \ P = \P" +unfolding stable_def defs by (metis suffix_zero) + +(* FIXME Sistla's examples of stable properties are boring and follow directly from this lemma. + FIXME the fairness "type of formulas" follow from the above and the fairness def. *) + +text\ + +To show that @{const \weakly_fair\} is a @{const \fairness\} property requires some constraints on \enabled\ and \taken\: +\<^item> it is reasonable to assume they are state formulas +\<^item> \taken\ must be satisfiable + +\ + +lemma fairness_weakly_fair: + assumes "\s. taken s" + shows "fairness (weakly_fair \enabled\ \taken\)" +unfolding fairness_def stable_def absolute_liveness_def weakly_fair_def +using assms +apply auto + apply (rule_tac x="\_ .s" in exI) + apply fastforce + apply (simp add: alwaysD) + apply (rule_tac x="\_ .s" in exI) + apply fastforce +apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def) +done + +lemma fairness_strongly_fair: + assumes "\s. taken s" + shows "fairness (strongly_fair \enabled\ \taken\)" +unfolding fairness_def stable_def absolute_liveness_def strongly_fair_def +using assms +apply auto + apply (rule_tac x="\_ .s" in exI) + apply fastforce + apply (simp add: alwaysD) + apply (rule_tac x="\_ .s" in exI) + apply fastforce +apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def) +done + +(*<*) + +end +(*>*) diff --git a/thys/ConcurrentIMP/ROOT b/thys/ConcurrentIMP/ROOT --- a/thys/ConcurrentIMP/ROOT +++ b/thys/ConcurrentIMP/ROOT @@ -1,11 +1,14 @@ chapter AFP session ConcurrentIMP (AFP) = "HOL-Library" + options [timeout = 300] + directories + "ex" theories [show_question_marks = false, names_short] CIMP - CIMP_one_place_buffer_ex - CIMP_unbounded_buffer_ex + "ex/CIMP_locales" + "ex/CIMP_one_place_buffer" + "ex/CIMP_unbounded_buffer" document_files "root.bib" "root.tex" diff --git a/thys/ConcurrentIMP/cimp.ML b/thys/ConcurrentIMP/cimp.ML new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/cimp.ML @@ -0,0 +1,140 @@ +(* Pollutes the global namespace, but we use them everywhere *) +fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; +fun HOL_ss_only thms ctxt = clear_simpset (put_simpset HOL_ss ctxt) addsimps thms; + +signature CIMP = +sig + val com_locs_fold : (term * 'b -> 'b) -> 'b -> term -> 'b + val com_locs_map : (term -> 'b) -> term -> 'b list + val com_locs_fold_no_response : (term * 'b -> 'b) -> 'b -> term -> 'b + val com_locs_map_no_response : (term -> 'b) -> term -> 'b list + val intern_com : Facts.ref -> local_theory -> local_theory + val def_locset : thm -> local_theory -> local_theory +end; + +structure Cimp : CIMP = +struct + +fun com_locs_fold f x (Const (@{const_name Request}, _) $ l $ _ $ _ ) = f (l, x) + | com_locs_fold f x (Const (@{const_name Response}, _) $ l $ _) = f (l, x) + | com_locs_fold f x (Const (@{const_name LocalOp}, _) $ l $ _) = f (l, x) + | com_locs_fold f x (Const (@{const_name Cond1}, _) $ l $ _ $ c) = com_locs_fold f (f (l, x)) c + | com_locs_fold f x (Const (@{const_name Cond2}, _) $ l $ _ $ c1 $ c2) = com_locs_fold f (com_locs_fold f (f (l, x)) c1) c2 + | com_locs_fold f x (Const (@{const_name Loop}, _) $ c) = com_locs_fold f x c + | com_locs_fold f x (Const (@{const_name While}, _) $ l $ _ $ c) = com_locs_fold f (f (l, x)) c + | com_locs_fold f x (Const (@{const_name Seq}, _) $ c1 $ c2) = com_locs_fold f (com_locs_fold f x c1) c2 + | com_locs_fold f x (Const (@{const_name Choose}, _) $ c1 $ c2) = com_locs_fold f (com_locs_fold f x c1) c2 + | com_locs_fold _ x _ = x; + +fun com_locs_map f com = com_locs_fold (fn (l, acc) => f l :: acc) [] com + +fun com_locs_fold_no_response f x (Const (@{const_name Request}, _) $ l $ _ $ _ ) = f (l, x) + | com_locs_fold_no_response _ x (Const (@{const_name Response}, _) $ _ $ _) = x (* can often ignore \Response\ *) + | com_locs_fold_no_response f x (Const (@{const_name LocalOp}, _) $ l $ _) = f (l, x) + | com_locs_fold_no_response f x (Const (@{const_name Cond1}, _) $ l $ _ $ c) = com_locs_fold_no_response f (f (l, x)) c + | com_locs_fold_no_response f x (Const (@{const_name Cond2}, _) $ l $ _ $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f (f (l, x)) c1) c2 + | com_locs_fold_no_response f x (Const (@{const_name Loop}, _) $ c) = com_locs_fold_no_response f x c + | com_locs_fold_no_response f x (Const (@{const_name While}, _) $ l $ _ $ c) = com_locs_fold_no_response f (f (l, x)) c + | com_locs_fold_no_response f x (Const (@{const_name Seq}, _) $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2 + | com_locs_fold_no_response f x (Const (@{const_name Choose}, _) $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2 + | com_locs_fold_no_response _ x _ = x; + +fun com_locs_map_no_response f com = com_locs_fold_no_response (fn (l, acc) => f l :: acc) [] com + +fun cprop_of_equality ctxt : thm -> cterm = + Local_Defs.meta_rewrite_rule ctxt (* handle `=` or `\` *) + #> Thm.cprop_of + +fun equality_lhs ctxt : thm -> term = + cprop_of_equality ctxt #> Thm.dest_equals_lhs #> Thm.term_of + +fun equality_rhs ctxt : thm -> term = + cprop_of_equality ctxt #> Thm.dest_equals_rhs #> Thm.term_of + +(* Intern all labels mentioned in CIMP programs \facts\ + +FIXME can only use \com_intern\ once per locale +FIXME forces all labels to be unique and distinct from other constants in the locale. +FIXME assumes the labels are character strings +*) +fun intern_com facts ctxt : local_theory = + let + val thms = Proof_Context.get_fact ctxt facts + (* Define constants with defs of the form loc.XXX_def: "XXX \ ''XXX''. *) + val attrs = [] + fun add_literal_def (literal, (loc_defs, ctxt)) : thm list * local_theory = + let + val literal_name = HOLogic.dest_string literal (* FIXME might not be a nice name, but the error is readable so shrug. FIXME generalise to other label types *) + val literal_def_binding = Binding.empty (* Binding.qualify true "loc" (Binding.name (Thm.def_name literal_name)) No need to name individual defs *) + val ((_, (_, loc_def)), ctxt) = Local_Theory.define ((Binding.name literal_name, Mixfix.NoSyn), ((literal_def_binding, attrs), literal)) ctxt + in + (loc_def :: loc_defs, ctxt) + end; + val (loc_defs, ctxt) = List.foldl (fn (com, acc) => com_locs_fold add_literal_def acc (equality_rhs ctxt com)) ([], ctxt) thms + + val coms_interned = List.map (Local_Defs.fold ctxt loc_defs) thms + val attrs = [] + val (_, ctxt) = Local_Theory.note ((@{binding "loc_defs"}, attrs), loc_defs) ctxt + val (_, ctxt) = Local_Theory.note ((@{binding "com_interned"}, attrs), coms_interned) ctxt + in + ctxt + end; + +(* Cache location set membership facts. + +Decide membership in the given set for each label in the CIMP programs +in the Named_Theorems "com". + +If the label set and com types differ, we probably get a nasty error. + +*) + +fun def_locset thm ctxt = + let + val set_name = equality_lhs ctxt thm + val set_name_str = case set_name of Const (c, _) => c | Free (c, _) => c | _ => error ("Not an equation of the form x = set: " ^ Thm.string_of_thm ctxt thm) + val memb_thm_name = Binding.qualify true set_name_str (Binding.name "memb") + fun mk_memb l = Thm.cterm_of ctxt (HOLogic.mk_mem (l, set_name)) +(* +1. solve atomic membership yielding \''label'' \ set\ or \''label'' \ set\. +2. fold \loc_defs\ +3. cleanup with the existing \locset_cache\. +FIXME trim simpsets: 1: sets 2: not much 3: not much +*) + val loc_defs = Proof_Context.get_fact ctxt (Facts.named "loc_defs") + val membership_ctxt = ctxt addsimps ([thm] @ loc_defs) + val cleanup_ctxt = HOL_ss_only (@{thms cleanup_simps} @ Named_Theorems.get ctxt \<^named_theorems>\locset_cache\) ctxt + val rewrite_tac = + Simplifier.rewrite membership_ctxt + #> Local_Defs.fold ctxt loc_defs + #> Simplifier.simplify cleanup_ctxt + val coms = Proof_Context.get_fact ctxt (Facts.named "com_interned") +(* Parallel *) + fun mk_thms coms : thm list = Par_List.map rewrite_tac (maps (equality_rhs ctxt #> com_locs_map_no_response mk_memb) coms) +(* Sequential *) +(* fun mk_thms coms = List.foldl (fn (c, thms) => com_locs_fold (fn l => fn thms => rewrite_tac (mk_memb l) :: thms) thms c) [] coms *) + val attrs = [] + val (_, ctxt) = ctxt |> Local_Theory.note ((memb_thm_name, attrs), mk_thms coms) +(* Add \memb_thms\ to the global (and inherited by locales) \locset_cache\ *) + val memb_thm_full_name = Local_Theory.full_name ctxt memb_thm_name + val (finish, ctxt) = Target_Context.switch_named_cmd (SOME ("-", Position.none)) (Context.Proof ctxt) (* switch to the "root" local theory *) + val memb_thms = Proof_Context.get_fact ctxt (Facts.named memb_thm_full_name) + val attrs = [Attrib.internal (K (Named_Theorems.add \<^named_theorems>\locset_cache\))] + val (_, ctxt) = ctxt |> Local_Theory.note ((Binding.empty, attrs), memb_thms) + val ctxt = case finish ctxt of Context.Proof ctxt => ctxt | _ => error "Context.generic failure" (* Return to the locale we were in *) + in + ctxt + end; + +end; + +val _ = + Outer_Syntax.local_theory \<^command_keyword>\intern_com\ "intern labels in CIMP commands" + (Parse.thms1 >> (fn facts => fn ctxt => List.foldl (fn ((f, _), ctxt) => Cimp.intern_com f ctxt) ctxt facts)); + +val _ = + Outer_Syntax.local_theory' \<^command_keyword>\locset_definition\ "constant definition for sets of locations" + (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- + Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy => + Specification.definition_cmd decl params prems spec b lthy + |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_locset)); diff --git a/thys/ConcurrentIMP/document/root.bib b/thys/ConcurrentIMP/document/root.bib --- a/thys/ConcurrentIMP/document/root.bib +++ b/thys/ConcurrentIMP/document/root.bib @@ -1,533 +1,656 @@ @STRING{cacm="Communications of the ACM"} +@STRING{csur="{ACM} Computing Surveys"} +@STRING{fac="Formal Aspects of Computing"} +@STRING{ipl="Information Processing Letters"} +@STRING{lncs="LNCS"} +@STRING{tcs="Theoretical Computer Science"} @article{AptFrancezDeRoever:1980, author = {K. R. Apt and Francez, N. and de Roever, W. P.}, title = {A Proof System for Communicating Sequential Processes}, journal = toplas, year = 1980, volume = 2, number = 3, pages = {359--385}, doi = {10.1145/357103.357110} } @TechReport{LynchTuttle:1989, author = "Lynch, N. A and Tuttle, M. R.", - title = "An introduction to - input/output automata", + title = "An introduction to input/output automata", institution = "CWI", year = 1989, month = sep, annote = "CWI Quarterly 2 (3): 219–246", url = "http://www.markrtuttle.com/data/papers/lt89-cwi.pdf" } @book{Lynch:1996, author = {N. A. Lynch}, title = {Distributed Algorithms}, - year = {1996}, + year = 1996, publisher = {Morgan Kaufmann Publishers Inc.}, } @InProceedings{PrenEsp00, author = {Prensa Nieto, L. and J. Esparza}, title = {Verifying Single and Multi-mutator Garbage Collectors with {Owicki/Gries} in {Isabelle/HOL}}, booktitle = {Mathematical Foundations of Computer Science (MFCS 2000)}, editor = {M. Nielsen and B. Rovan}, - publisher = {Springer-Verlag}, - series = {LNCS}, + publisher = {Springer}, + series = lncs, volume = 1893, pages = {619--628}, year = 2000 } -@PhdThesis{Prensa-PhD,author={Prensa Nieto, L.}, -title={Verification of Parallel Programs with the Owicki-Gries and -Rely-Guarantee Methods in Isabelle/HOL}, -school={Technische Universit{\"a}t M{\"u}nchen},year=2002} +@PhdThesis{Prensa-PhD, + author={Prensa Nieto, L.}, + title={Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL}, + school={Technische Universit{\"a}t M{\"u}nchen}, + year=2002 +} -@inproceedings{Prensa-ESOP03,author={Prensa Nieto, L.}, -title={The {Rely-Guarantee} Method in {Isabelle/HOL}}, -booktitle={European Symposium on Programming (ESOP'03)},editor={P. Degano}, -publisher=Springer,series=LNCS,volume=2618,pages={348--362},year=2003} +@inproceedings{Prensa-ESOP03, + author={Prensa Nieto, L.}, + title={The {Rely-Guarantee} Method in {Isabelle/HOL}}, + booktitle={ESOP'2003}, + editor={P. Degano}, + publisher="Springer", + series=lncs,volume=2618, + pages={348--362}, + year=2003 +} @book{Winskel:1993, author = {Winskel, G.}, title = {The Formal Semantics of Programming Languages}, - year = {1993}, + year = 1993, publisher = {MIT Press}, address = "Cambridge, MA" } @article{DBLP:journals/cacm/DijkstraLMSS78, author = {E. W. Dijkstra and L. Lamport and A. J. Martin and C. S. Scholten and E. F. M. Steffens}, title = {On-the-Fly Garbage Collection: An Exercise in Cooperation}, journal = cacm, - volume = {21}, - number = {11}, - year = {1978}, + volume = 21, + number = 11, + year = 1978, pages = {966-975}, ee = {http://doi.acm.org/10.1145/359642.359655}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/lpar/Schirmer04, author = {N. Schirmer}, title = {A Verification Environment for Sequential Imperative Programs in Isabelle/HOL}, booktitle = {LPAR}, - year = {2004}, + year = 2004, pages = {398-414}, ee = {https://doi.org/10.1007/978-3-540-32275-7_26}, crossref = {DBLP:conf/lpar/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {3-540-25236-3}, @proceedings{DBLP:conf/lpar/2004, editor = {F. Baader and A. Voronkov}, title = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings}, booktitle = {LPAR}, publisher = {Springer}, series = lncs, volume = {3452}, year = {2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/cacm/SewellSONM10, author = {P. Sewell and S. Sarkar and S. Owens and F. Zappa Nardelli and M. O. Myreen}, title = {{x86-TSO}: a rigorous and usable programmer's model for x86 multiprocessors}, journal = cacm, volume = {53}, number = {7}, year = {2010}, pages = {89-97}, ee = {http://doi.acm.org/10.1145/1785414.1785443}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/mfcs/BoerRH99, author = {de Boer, F. S. and de Roever, W. P. and U. Hannemann}, title = {The Semantic Foundations of a Compositional Proof Method for Synchronously Communicating Processes}, booktitle = {MFCS}, year = {1999}, pages = {343-353}, ee = {https://doi.org/10.1007/3-540-48340-3_31}, crossref = {DBLP:conf/mfcs/1999}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {3-540-66408-4}, @proceedings{DBLP:conf/mfcs/1999, editor = {M. Kutylowski and L. Pacholski and T. Wierzbicki}, title = {Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS'99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings}, booktitle = {MFCS}, publisher = {Springer}, series = lncs, volume = {1672}, year = {1999}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {0-521-80608-9}, -@book{DBLP:books/cu/RoeverBH2001, +@book{deRoeverEtAl:2001, author = {de Roever, W. P. and de Boer, F. S. and U. Hannemann and J. Hooman and Y. Lakhnech and M. Poel and J. Zwiers}, title = {Concurrency Verification: Introduction to Compositional and Noncompositional Methods}, publisher = {Cambridge University Press}, series = {Cambridge Tracts in Theoretical Computer Science}, - volume = {54}, - year = {2001}, - bibsource = {DBLP, http://dblp.uni-trier.de} + volume = 54, + year = 2001, } @InProceedings{Pizlo+2010PLDI, author = {F. Pizlo and L. Ziarek and P. Maj and A. L. Hosking and E. Blanton and J. Vitek}, title = {Schism: Fragmentation-Tolerant Real-Time Garbage Collection}, booktitle = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation}, year = 2010, pages = "146--159", month = jun, address = {Toronto, Canada}, doi = {10.1145/1806596.1806615} } @PhdThesis{Pizlo201xPhd, author = {F. Pizlo}, title = {Fragmentation Tolerant Real Time Garbage Collection}, school = {Purdue University}, year = {201x} } @article{DBLP:journals/toplas/LamportS84, - author = {L. Lamport and - F. B. Schneider}, + author = {L. Lamport and F. B. Schneider}, title = {The ``{Hoare Logic}'' of {CSP}, and All That}, journal = toplas, volume = {6}, number = {2}, year = {1984}, pages = {281-296}, ee = {http://doi.acm.org/10.1145/2993.357247}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/acta/Lamport80, author = {L. Lamport}, title = {The ``{Hoare Logic}'' of Concurrent Programs}, journal = {Acta Informatica}, volume = {14}, year = {1980}, pages = {21-37}, ee = {https://doi.org/10.1007/BF00289062}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/jar/Berghofer12, author = {S. Berghofer}, title = {A Solution to the {PoplMark} Challenge Using {de Bruijn} Indices in {Isabelle/HOL}}, journal = {J. Autom. Reasoning}, volume = {49}, number = {3}, year = {2012}, pages = {303-326}, ee = {https://doi.org/10.1007/s10817-011-9231-4}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {3-540-44044-5} @InCollection{PittsAM:opespe, author = {A. M. Pitts}, title = {Operational Semantics and Program Equivalence}, booktitle = {Applied Semantics, Advanced Lectures}, pages = {378--412}, - publisher = {Springer-Verlag}, + publisher = {Springer}, year = 2002, editor = {G. Barthe and P. Dybjer and J. Saraiva}, volume = 2395, series = lncs, note = {International Summer School, {APPSEM} 2000, Caminha, Portugal, September 9--15, 2000}, } +@InCollection{MannaPnueli:1991, + author = "Z. Manna and A. Pnueli", + title = "Tools and rules for the practicing verifier", + booktitle = "CMU Computer Science: A 25th Anniversary Commemorative", + pages = "121–-156", + publisher = "ACM Press and Addison-Wesley", + year = 1991, + editor = "R. F. Rashid", + note = "Also Technical Report STAN-CS-90-1321" +} + % isbn = {978-0-387-94459-3}, @book{MannaPnueli:1995, author = {Z. Manna and A. Pnueli}, - title = {Temporal verification of reactive systems - safety}, + title = {Temporal verification of reactive systems - {Safety}}, publisher = {Springer}, year = 1995, pages = {I-XV, 1-512}, } +@inproceedings{MannaPnueli:2010, + author = {Z. Manna and A. Pnueli}, + title = {Temporal Verification of Reactive Systems: Response}, + booktitle = {Time for Verification, Essays in Memory of Amir Pnueli}, + series = lncs, + volume = 6200, + publisher = {Springer}, + pages = {279--361}, + year = 2010, + doi = {10.1007/978-3-642-13754-9\_13}, +} + @article{DBLP:journals/acta/LevinG81, author = {G. Levin and D. Gries}, title = {A Proof Technique for Communicating Sequential Processes}, journal = {Acta Inf.}, volume = {15}, year = {1981}, pages = {281-302}, ee = {https://doi.org/10.1007/BF00289266}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{CousotCousot:1980, author = {P. Cousot and R. Cousot}, title = "Semantic Analysis of {Communicating Sequential Processes} (Shortened Version)", booktitle = {ICALP}, series = lncs, volume = {85}, publisher = {Springer}, year = 1980, pages = {119-133}, ee = {https://doi.org/10.1007/3-540-10003-2_65}, } -@InCollection{MannaPnueli:1991, - author = "Z. Manna and A. Pnueli", - title = "Tools and rules for the practicing verifier", - booktitle = "CMU Computer Science: A 25th Anniversary Commemorative", - pages = "121–-156", - publisher = "ACM Press and Addison-Wesley", - year = 1991, - editor = "R. F. Rashid" -} - % isbn = {0-3211-4306-X}, -@book{DBLP:books/aw/Lamport2002, +@book{Lamport:2002, author = {L. Lamport}, title = {Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers}, publisher = {Addison-Wesley}, - year = {2002}, - bibsource = {DBLP, http://dblp.uni-trier.de} + year = 2002 } @article{TLA-AFP, author = {G. Grov and S. Merz}, title = {A Definitional Encoding of TLA* in Isabelle/HOL}, journal = {Archive of Formal Proofs}, month = nov, year = 2011, note = {\url{http://isa-afp.org/entries/TLA}, Formal proof development}, ISSN = {2150-914x}, } @inproceedings{DBLP:conf/itp/CohenS10, author = {E. Cohen and B. Schirmer}, title = {From Total Store Order to Sequential Consistency: A Practical Reduction Theorem}, booktitle = {ITP}, year = {2010}, pages = {403-418}, ee = {https://doi.org/10.1007/978-3-642-14052-5_28}, crossref = {DBLP:conf/itp/2010}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {978-3-642-14051-8}, @proceedings{DBLP:conf/itp/2010, editor = {M. Kaufmann and L. C. Paulson}, title = {Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, booktitle = {ITP}, publisher = {Springer}, series = lncs, volume = {6172}, year = {2010}, ee = {https://doi.org/10.1007/978-3-642-14052-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/fase/NipkowN99, author = {T. Nipkow and Prensa Nieto, L.}, title = "{Owicki/Gries} in {Isabelle/HOL}", booktitle = {FASE}, year = {1999}, pages = {188-203}, ee = {https://doi.org/10.1007/978-3-540-49020-3_13}, crossref = {DBLP:conf/fase/1999}, bibsource = {DBLP, http://dblp.uni-trier.de} } % isbn = {3-540-65718-5}, @proceedings{DBLP:conf/fase/1999, editor = {J.-P. Finance}, title = {Fundamental Approaches to Software Engineering, Second Internationsl Conference, FASE'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings}, booktitle = {FASE}, publisher = {Springer}, series = lncs, volume = {1577}, year = {1999}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{CousotCousot89-IC, author = {Cousot, P. and Cousot, R.}, title = {A language independent proof of the soundness and completeness of generalized {H}oare logic}, journal = {Information and Computation}, volume = 80, number = 2, pages = {165--191}, month = feb, year = 1989, } -@inproceedings{DBLP:conf/popl/DoligezG94, - author = {D. Doligez and - G. Gonthier}, - title = {Portable, Unobtrusive Garbage Collection for Multiprocessor - Systems}, - booktitle = {POPL}, - year = {1994}, - pages = {70-83}, - ee = {http://doi.acm.org/10.1145/174675.174673}, - crossref = {DBLP:conf/popl/1994}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -% isbn = {0-89791-636-0}, -@proceedings{DBLP:conf/popl/1994, - editor = {Boehm, H.-J. and - B. Lang and - D. M. Yellin}, - title = {Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium - on Principles of Programming Languages, Portland, Oregon, - USA, January 17-21, 1994}, - booktitle = popl, - publisher = {ACM Press}, - year = {1994}, - ee = {http://dl.acm.org/citation.cfm?id=174675}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - @article{DBLP:journals/jlp/Plotkin04, author = {G. D. Plotkin}, title = {The origins of structural operational semantics}, journal = {Journal of Logic and Algebraic Programming}, volume = {60-61}, year = {2004}, pages = {3-15}, ee = {https://doi.org/10.1016/j.jlap.2004.03.009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Book{ConcreteSemantics:2014, - author = "T. Nipkow and G. Klein", + author = "T. Nipkow and G. Klein", title = "Concrete Semantics: A Proof Assistant Approach", - publisher = Springer, + publisher = "Springer", year = 2014, url = "http://www.in.tum.de/~nipkow/Concrete-Semantics/" } @Book{Hoare:1985, author = {C.A.R. Hoare}, title = "{Communicating Sequential Processes}", publisher = {Prentice-Hall}, - year = 1985, + year = 1985, series = {International Series In Computer Science}, url = "http://www.usingcsp.com/" } @Book{Milner:1980, - author = "R. Milner", + author = "R. Milner", title = "A Calculus of Communicating Systems", - publisher = Springer, + publisher = "Springer", year = 1980 } @book{Milner:1989, author = {R. Milner}, title = "Communication and Concurrency", year = {1989}, publisher = {Prentice-Hall}, address = "Englewood Cliffs, NJ", } -@article{DBLP:journals/tcs/FelleisenH92, +@article{FelleisenHieb:1992, author = {M. Felleisen and R. Hieb}, title = {The Revised Report on the Syntactic Theories of Sequential Control and State}, - journal = {Theor. Comput. Sci.}, - volume = {103}, - number = {2}, - year = {1992}, + journal = tcs, + volume = 103, + number = 2, + year = 1992, pages = {235-271}, - ee = {https://doi.org/10.1016/0304-3975(92)90014-7}, - bibsource = {DBLP, http://dblp.uni-trier.de} + doi = {10.1016/0304-3975(92)90014-7}, } -@inproceedings{DBLP:conf/tphol/Jackson98, - author = {Paul B. Jackson}, +@inproceedings{Jackson:1998, + author = {P. B. Jackson}, title = {Verifying a Garbage Collection Algorithm}, booktitle = {TPHOLs}, - year = {1998}, - pages = {225-244}, - ee = {https://doi.org/10.1007/BFb0055139}, - crossref = {DBLP:conf/tphol/1998}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/tphol/1998, - editor = {Jim Grundy and - Malcolm C. Newey}, - title = {Theorem Proving in Higher Order Logics, 11th International - Conference, TPHOLs'98, Canberra, Australia, September 27 - - October 1, 1998, Proceedings}, - booktitle = {TPHOLs}, publisher = {Springer}, - series = {Lecture Notes in Computer Science}, + series = lncs, volume = {1479}, - year = {1998}, - isbn = {3-540-64987-5}, - bibsource = {DBLP, http://dblp.uni-trier.de} + year = 1998, + pages = {225-244}, + doi = {10.1007/BFb0055139}, } -@article{DBLP:journals/logcom/Coupet-GrimalN03, - author = {Coupet-Grimal, S. and - Nouvet, C.}, - title = {Formal Verification of an Incremental Garbage Collector}, - journal = {J. Log. Comput.}, - volume = {13}, - number = {6}, - year = {2003}, - pages = {815-833}, - ee = {https://doi.org/10.1093/logcom/13.6.815}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@article{DBLP:journals/logcom/Coupet-Grimal03, +@article{CoupetGrimal:2003, author = {Coupet-Grimal, S.}, - title = {An Axiomatization of Linear Temporal Logic in the Calculus - of Inductive Constructions}, - journal = {J. Log. Comput.}, - volume = {13}, - number = {6}, - year = {2003}, + title = {An Axiomatization of {Linear Temporal Logic} in the {Calculus + of Inductive Constructions}}, + journal = {Journal of Logic and Computation}, + volume = 13, + number = 6, + year = 2003, pages = {801-813}, - ee = {https://doi.org/10.1093/logcom/13.6.801}, - bibsource = {DBLP, http://dblp.uni-trier.de} + doi = {10.1093/logcom/13.6.801}, } @article{DBLP:journals/entcs/SchirmerW09, author = {N. Schirmer and M. Wenzel}, title = {State Spaces - The Locale Way}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {254}, year = {2009}, pages = {161-179}, ee = {https://doi.org/10.1016/j.entcs.2009.09.065}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{Ridge:2009, author = {T. Ridge}, title = {Verifying distributed systems: the operational approach}, booktitle = {POPL'2009}, pages = {429--440}, publisher = {{ACM}}, year = 2009, doi = {10.1145/1480881.1480934}, } + +@book{ChandyMisra:1989, + author = {Chandy, K. M. and Misra, J.}, + title = {Parallel program design - a foundation}, + publisher = {Addison-Wesley}, + year = 1989, + isbn = {978-0-201-05866-6}, +} + +% 2019-06 FIXME not yet published? +@Article{vanGlabbeekHofner:2019, + author = {van Glabbeek, R. J. and H\"{o}fner, P.}, + title = {Progress, Justness and Fairness}, + journal = csur, + year = 2019, + url = {http://arxiv.org/abs/1810.07414v1} +} + +@article{AptDelporteGallet:1986, + author = {Krzysztof R. Apt and + Carole Delporte{-}Gallet}, + title = {Syntax Directed Analysis of Liveness Properties}, + journal = {Information and Control}, + volume = 68, + number = {1-3}, + pages = {223--253}, + year = 1986, + doi = {10.1016/S0019-9958(86)80037-7}, +} + +@inproceedings{MisraChandySmith:1982, + author = {J. Misra and + K. M. Chandy and + T. Smith}, + title = {Proving Safety and Liveness of Communicating Processes with Examples}, + booktitle = {PODC'1982}, + publisher = {{ACM}}, + pages = {201--208}, + year = 1982, + doi = {10.1145/800220.806698}, +} + +@article{AlpernSchneider:1985, + author = {B. Alpern and + F. B. Schneider}, + title = {Defining Liveness}, + journal = ipl, + volume = 21, + number = 4, + pages = {181--185}, + year = 1985, + doi = {10.1016/0020-0190(85)90056-0}, +} + +@TechReport{Schneider:1987, + author = {F. B. Schneider}, + title = {Decomposing Properties into Safety and Liveness using Predicate Logic}, + institution = {Department of Computer Science, Cornell University}, + year = 1987, + number = {87-874}, + month = oct +} + +% FIXME guesswork on some of the biblio data +@article{Kindler:1994, + author = {E. Kindler}, + title = {Safety and liveness properties: A survey}, + journal = {Bulletin of the European Association for Theoretical Computer Science}, + year = 1994, + volume = 53, + number = 30, + pages = {268--272}, + month = 6, + url = "http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.8206&rep=rep1&type=pdf", +} + +@article{Sistla:1994, + author = {Sistla, A. P.}, + title = {Safety, Liveness and Fairness in Temporal Logic}, + journal = fac, + volume = 6, + number = 5, + pages = {495--512}, + year = 1994, + doi = {10.1007/BF01211865}, +} + +@article{OwickiLamport:1982, + author = {S. S. Owicki and + L. Lamport}, + title = {Proving Liveness Properties of Concurrent Programs}, + journal = toplas, + volume = 4, + number = 3, + pages = {455--495}, + year = 1982, + doi = {10.1145/357172.357178}, +} + +@inproceedings{ChangMannaPnueli:1992, + author = {E. Y. Chang and + Z. Manna and + A. Pnueli}, + title = {Characterization of Temporal Property Classes}, + booktitle = {ICALP'1992}, + pages = {474--486}, + year = 1992, + series = lncs, + volume = 623, + publisher = {Springer}, + doi = {10.1007/3-540-55719-9\_97}, +} + +@inproceedings{MannaPnueli:1988, + author = {Z. Manna and + A. Pnueli}, + title = {The anchored version of the temporal framework}, + booktitle = {Linear Time, Branching Time and Partial Order in Logics and Models + for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, + May 30 - June 3, 1988, Proceedings}, + editor = {de Bakker, J. W. and + de Roever, W. P. and + Rozenberg, G.}, + pages = {201--284}, + year = 1988, + doi = {10.1007/BFb0013024}, + volume = 354, + publisher = {Springer}, + series = lncs, +} + +@inproceedings{PnueliArons:2003, + author="Pnueli, A. and Arons, T.", + title="{TLPVS}: A {PVS}-Based {LTL} Verification System", + bookTitle="Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday", + year=2003, + publisher="Springer", + series=lncs, + volume=2772, + address="Berlin, Heidelberg", + pages="598--625", + abstract="In this paper we present our pvs implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive ltl system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems --- systems in which the number of processes is unbounded --- and our verification rules are appropriate to such systems.", + isbn="978-3-540-39910-0", + doi="10.1007/978-3-540-39910-0_26", +} + +@article{AbadiPlotkin:1993, + author = {Mart{\'{\i}}n Abadi and + Gordon D. Plotkin}, + title = {A Logical View of Composition}, + journal = tcs, + volume = 114, + number = 1, + pages = {3--30}, + year = 1993, + doi = {10.1016/0304-3975(93)90151-I}, + note = {Journal version of FIXME Abadi, Plotkin (POPL, 1991)} +} diff --git a/thys/ConcurrentIMP/document/root.tex b/thys/ConcurrentIMP/document/root.tex --- a/thys/ConcurrentIMP/document/root.tex +++ b/thys/ConcurrentIMP/document/root.tex @@ -1,87 +1,88 @@ \documentclass[11pt,a4paper]{article} \usepackage[a4paper,margin=1cm,footskip=.5cm]{geometry} \usepackage{isabelle,isabellesym} \usepackage{amssymb} +\usepackage{wasysym} \usepackage[english]{babel} % lifted composition. \newcommand{\isasymbigcirc}{\isamath{\circ}} % Bibliography \usepackage[authoryear,longnamesfirst,sort]{natbib} \bibpunct();A{}, % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \renewcommand{\ttdefault}{cmtt} % CM rather than courier for \tt % for uniform font size \renewcommand{\isastyle}{\isastyleminor} % Abstract various things that might change. \newcommand{\ccode}[1]{\texttt{#1}} \newcommand{\isabelletype}[1]{\emph{#1}} \newcommand{\isabelleterm}[1]{\emph{#1}} \begin{document} \title{CIMP} \author{Peter Gammie} \maketitle \begin{abstract} CIMP extends the small imperative language IMP with control non-determinism and constructs for synchronous message passing. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} \section{Concluding remarks} Previously \citet{DBLP:conf/fase/NipkowN99,Prensa-PhD,Prensa-ESOP03}\footnote{The theories are in \texttt{\$ISABELLE/src/HOL/Hoare\_Parallel}.} have developed the classical Owicki/Gries and Rely-Guarantee paradigms for the verification of shared-variable concurrent programs in Isabelle/HOL. These have been used to show the correctness of a garbage collector \citep{PrenEsp00}. We instead use synchronous message passing, which is significantly less explored. \citet{DBLP:conf/mfcs/BoerRH99,DBLP:books/cu/RoeverBH2001} provide compositional systems for \emph{terminating} systems. We have instead adopted Lamport's paradigm of a single global invariant and local proof obligations as the systems we have in mind are tightly coupled and it is not obvious that the proofs would be easier on a decomposed system; see \citet[\S1.6.6]{DBLP:books/cu/RoeverBH2001} for a concurring opinion. Unlike the generic sequential program verification framework Simpl \citep{DBLP:conf/lpar/Schirmer04}, we do not support function calls, or a sophisticated account of state spaces. Moreover we do no meta-theory beyond showing the simple VCG is sound (\S\ref{sec:cimp-vcg}). \bibliographystyle{plainnat} \bibliography{root} \addcontentsline{toc}{section}{References} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/ConcurrentIMP/ex/CIMP_locales.thy b/thys/ConcurrentIMP/ex/CIMP_locales.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/ex/CIMP_locales.thy @@ -0,0 +1,60 @@ +(*<*) +theory CIMP_locales +imports + "../CIMP" +begin + +(*>*) +section\ One locale per process \ + +text\ + +A sketch of what we're doing in \ConcurrentGC\, for quicker testing. + +FIXME write some lemmas that further exercise the generated thms. + +\ + +locale P1 +begin + +definition com :: "(unit, string, unit, nat) com" where + "com = \''A''\ WHILE ((<) 0) DO \''B''\ \\s. s - 1\ OD" + +intern_com com_def +print_theorems (* P1.com_interned, P1.loc_defs *) + +locset_definition "loop = {B}" +print_theorems (* P1.loop.memb, P1.loop_def *) +thm locset_cache (* the two facts in P1.loop.memb *) + +definition "assertion = atS False loop" + +end + +thm locset_cache (* the two facts in P1.loop.memb *) + +locale P2 +begin + +thm locset_cache (* the two facts in P1.loop.memb *) + +definition com :: "(unit, string, unit, nat) com" where + "com = \''C''\ WHILE ((<) 0) DO \''A''\ \Suc\ OD" + +intern_com com_def +locset_definition "loop = {A}" +print_theorems + +end + +thm locset_cache (* four facts: P1.loop.memb, P2.loop.memb *) + +primrec coms :: "bool \ (unit, string, unit, nat) com" where + "coms False = P1.com" +| "coms True = P2.com" + +(*<*) + +end +(*>*) diff --git a/thys/ConcurrentIMP/ex/CIMP_one_place_buffer.thy b/thys/ConcurrentIMP/ex/CIMP_one_place_buffer.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/ex/CIMP_one_place_buffer.thy @@ -0,0 +1,165 @@ +(*<*) +(* + * Copyright 2015, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +theory CIMP_one_place_buffer +imports + "../CIMP" +begin + +(*>*) +section\Example: a one-place buffer \label{sec:one_place_buffer}\ + +text\ + +To demonstrate the CIMP reasoning infrastructure, we treat the trivial +one-place buffer example of @{cite [cite_macro=citet] +\\S3.3\ "DBLP:journals/toplas/LamportS84"}. Note that the +semantics for our language is different to @{cite +[cite_macro=citeauthor] "DBLP:journals/toplas/LamportS84"}'s, who +treated a historical variant of CSP (i.e., not the one in @{cite +"Hoare:1985"}). + +We introduce some syntax for fixed-topology (static channel-based) +scenarios. + +\ + +abbreviation + rcv_syn :: "'location \ 'channel \ ('val \ 'state \ 'state) + \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_" [0,0,81] 81) +where + "\l\ ch\f \ \l\ Response (\q s. if fst q = ch then {(f (snd q) s, ())} else {})" + +abbreviation + snd_syn :: "'location \ 'channel \ ('state \ 'val) + \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_" [0,0,81] 81) +where + "\l\ ch\f \ \l\ Request (\s. (ch, f s)) (\ans s. {s})" + +text\ + +These definitions largely follow @{cite [cite_macro=citet] +"DBLP:journals/toplas/LamportS84"}. We have three processes +communicating over two channels. We enumerate program locations. + +\ + +datatype ex_chname = \12 | \23 +type_synonym ex_val = nat +type_synonym ex_ch = "ex_chname \ ex_val" +datatype ex_loc = r12 | r23 | s23 | s12 +datatype ex_proc = p1 | p2 | p3 + +type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_val) com" +type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_val) state_pred" +type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system_state" +type_synonym ex_sys = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system" +type_synonym ex_history = "(ex_ch \ unit) list" + +text\ + +We further specialise these for our particular example. + +\ + +primrec + ex_coms :: "ex_proc \ ex_pgm" +where + "ex_coms p1 = \s12\ \12\id" +| "ex_coms p2 = LOOP DO \r12\ \12\(\v _. v) ;; \s23\ \23\id OD" +| "ex_coms p3 = \r23\ \23\(\v _. v)" + +text\ + +Each process starts with an arbitrary initial local state. + +\ + +abbreviation ex_init :: "(ex_proc \ ex_val) \ bool" where + "ex_init \ \True\" + +abbreviation sys :: ex_sys where + "sys \ \PGMs = ex_coms, INIT = ex_init, FAIR = \True\\" (* FIXME add fairness hypotheses *) + +text\ + +The following adapts Kai Engelhardt's, from his notes titled +\emph{Proving an Asynchronous Message Passing Program Correct}, +2011. The history variable tracks the causality of the system, which I +feel is missing in Lamport's treatment. We tack on Lamport's invariant +so we can establish \Etern_pred\. + +\ + +abbreviation + filter_on_channel :: "ex_chname \ ex_state \ ex_val list" ("\_" [100] 101) +where + "\ch \ map (snd \ fst) \ filter ((=) ch \ fst \ fst) \ HST" + +definition IL :: ex_pred where + "IL = pred_conjoin [ + at p1 s12 \<^bold>\ LIST_NULL \\12 + , terminated p1 \<^bold>\ \\12 \<^bold>= (\s. [s\ p1]) + , at p2 r12 \<^bold>\ \\12 \<^bold>= \\23 + , at p2 s23 \<^bold>\ \\12 \<^bold>= \\23 \<^bold>@ (\s. [s\ p2]) \<^bold>\ (\s. s\ p1 = s\ p2) + , at p3 r23 \<^bold>\ LIST_NULL \\23 + , terminated p3 \<^bold>\ \\23 \<^bold>= (\s. [s\ p2]) \<^bold>\ (\s. s\ p1 = s\ p3) + ]" + +text\ + +If @{const p3} terminates, then it has @{const p1}'s value. This is +stronger than @{cite [cite_macro=citeauthor] +"DBLP:journals/toplas/LamportS84"}'s as we don't ask that the first +process has also terminated. + +\ + +definition Etern_pred :: ex_pred where + "Etern_pred = (terminated p3 \<^bold>\ (\s. s\ p1 = s\ p3))" + +text\ + +Proofs from here down. + +\ + +lemma correct_system: + assumes "IL sh" + shows "Etern_pred sh" +using assms unfolding Etern_pred_def IL_def by simp + +lemma IL_p1: "ex_coms, p1, lconst {} \ \IL\ \s12\ \12\(\s. s)" +apply (rule vcg.intros) +apply (rename_tac p') +apply (case_tac p'; clarsimp simp: IL_def atLs_def) +done + +lemma IL_p2: "ex_coms, p2, lconst {r12} \ \IL\ \s23\ \23\(\s. s)" +apply (rule vcg.intros) +apply (rename_tac p') +apply (case_tac p'; clarsimp simp: IL_def) +done + +lemma IL: "sys \\<^bsub>pre\<^esub> IL" +apply (rule VCG) + apply (clarsimp simp: IL_def atLs_def dest!: initial_stateD) +apply (rename_tac p) +apply (case_tac p; clarsimp simp: IL_p1 IL_p2) +done + +lemma IL_valid: "sys \ \\IL\" +by (rule valid_prerun_lift[OF IL]) + +(*<*) + +end +(*>*) diff --git a/thys/ConcurrentIMP/ex/CIMP_unbounded_buffer.thy b/thys/ConcurrentIMP/ex/CIMP_unbounded_buffer.thy new file mode 100644 --- /dev/null +++ b/thys/ConcurrentIMP/ex/CIMP_unbounded_buffer.thy @@ -0,0 +1,145 @@ +(*<*) +(* + * Copyright 2015, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +theory CIMP_unbounded_buffer +imports + "../CIMP" + "HOL-Library.Prefix_Order" +begin + +abbreviation (input) + Receive :: "'location \ 'channel \ ('val \ 'state \ 'state) + \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_" [0,0,81] 81) +where + "\l\ ch\f \ \l\ Response (\q s. if fst q = ch then {(f (snd q) s, ())} else {})" + +abbreviation (input) + Send :: "'location \ 'channel \ ('state \ 'val) \ ('state \ 'state) + \ (unit, 'location, 'channel \ 'val, 'state) com" ("\_\/ _\_" [0,0,81] 81) +where + "\l\ ch\f \ \l\ Request (\s. (ch, fst f s)) (\ans s. {snd f s})" + +(*>*) +section\Example: an unbounded buffer \label{sec:unbounded_buffer}\ + +text\ + +This is more literally Kai Engelhardt's example from his notes titled +\emph{Proving an Asynchronous Message Passing Program Correct}, 2011. + +\ + +datatype ex_chname = \12 | \23 +type_synonym ex_val = nat +type_synonym ex_ls = "ex_val list" +type_synonym ex_ch = "ex_chname \ ex_val" +datatype ex_loc = c1 | r12 | r23 | s23 | s12 +datatype ex_proc = p1 | p2 | p3 + +type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_ls) com" +type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) state_pred" +type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) system_state" +type_synonym ex_sys = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) system" +type_synonym ex_history = "(ex_ch \ unit) list" + +text\ + +The local state for the producer process contains all values produced; consider that ghost state. + +\ + +abbreviation (input) snoc :: "'a \ 'a list \ 'a list" where "snoc x xs \ xs @ [x]" + +primrec ex_coms :: "ex_proc \ ex_pgm" where + "ex_coms p1 = LOOP DO \c1\ LocalOp (\xs. {snoc x xs |x. True}) ;; \s12\ \12\(last, id) OD" +| "ex_coms p2 = LOOP DO \r12\ \12\snoc + \ \c1\ IF (\s. length s > 0) THEN \s23\ \12\(hd, tl) FI + OD" +| "ex_coms p3 = LOOP DO \r23\ \23\snoc OD" + +abbreviation ex_init :: "(ex_proc \ ex_ls) \ bool" where + "ex_init s \ \p. s p = []" + +abbreviation sys :: ex_sys where + "sys \ \PGMs = ex_coms, INIT = ex_init, FAIR = \True\\" (* FIXME add fairness hypotheses *) + +abbreviation + filter_on_channel :: "ex_chname \ ex_state \ ex_val list" ("\_" [100] 101) +where + "\ch \ map (snd \ fst) \ filter ((=) ch \ fst \ fst) \ HST" + +definition I_pred :: ex_pred where + "I_pred = pred_conjoin [ + at p1 c1 \<^bold>\ \\12 \<^bold>= (\s. s\ p1) + , at p1 s12 \<^bold>\ (\s. length (s\ p1) > 0 \ butlast (s\ p1) = (\\12) s) + , \\12 \<^bold>\ (\s. s\ p1) + , \\12 \<^bold>= \\23 \<^bold>@ (\s. s\ p2) + , at p2 s23 \<^bold>\ (\s. length (s\ p2) > 0) + , (\s. s\ p3) \<^bold>= \\23 + ]" + +text\ + +The local state of @{const "p3"} is some prefix of the local state of +@{const "p1"}. + +\ + +definition Etern_pred :: ex_pred where + "Etern_pred \ \s. s\ p3 \ s\ p1" + +lemma correct_system: + assumes "I_pred s" + shows "Etern_pred s" +using assms unfolding Etern_pred_def I_pred_def less_eq_list_def prefix_def by clarsimp + +lemma p1_c1[simplified, intro]: + "ex_coms, p1, lconst {s12} \ \I_pred\ \c1\ LocalOp (\xs. { snoc x xs |x. True })" +apply (rule vcg.intros) +apply (clarsimp simp: I_pred_def atS_def) +done + +lemma p1_s12[simplified, intro]: + "ex_coms, p1, lconst {c1} \ \I_pred\ \s12\ \12\(last, id)" +apply (rule vcg.intros) +apply (rename_tac p') +apply (case_tac p'; clarsimp) +apply (clarsimp simp: I_pred_def atS_def) +apply (metis Prefix_Order.prefix_snoc append.assoc append_butlast_last_id) +done + +lemma p2_s23[simplified, intro]: + "ex_coms, p2, lconst {c1, r12} \ \I_pred\ \s23\ \12\(hd, tl)" +apply (rule vcg.intros) +apply (rename_tac p') +apply (case_tac p'; clarsimp) +done + +lemma p2_pi4[intro]: + "ex_coms, p2, lcond {s23} {c1, r12} (\s. s \ []) \ \I_pred\ \c1\ IF (\s. s \ []) THEN c' FI" +apply (rule vcg.intros) +apply (clarsimp simp: I_pred_def atS_def split: lcond_splits) +done + +lemma I: "sys \\<^bsub>pre\<^esub> I_pred" +apply (rule VCG) + apply (clarsimp dest!: initial_stateD simp: I_pred_def atS_def) +apply (rename_tac p) +apply (case_tac p; auto) +done + +lemma I_valid: "sys \ \\I_pred\" +by (rule valid_prerun_lift[OF I]) + +(*<*) + +end +(*>*)