I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin (* N is the number of processes. *) consts N :: nat (* Processes are identified by natural numbers. A variable is a function over all natural numbers, not just those from [0, N). However, the definition of reachable below restricts updates to processes from [0, N) *) type_synonym 't var = "nat \<Rightarrow> 't" definition "Proc i \<longleftrightarrow> i < N" for i (* There's at least one process. *) axiomatization where proc_0: "Proc 0" (* Control state of a process. A process is at control state assign_x if it has not started, assign_y if it has executed its assignment to x but not to y, and done if it has finished. *) datatype pc_label = assign_x | assign_y | finished (* State of the system. *) record state = pc :: "pc_label var" x :: "nat var" y :: "nat var" definition "update_pc st i l = st\<lparr>pc := (pc st)(i := l)\<rparr>" definition "update_x st i v = st\<lparr>x := (x st)(i := v)\<rparr>" definition "update_y st i v = st\<lparr>y := (y st)(i := v)\<rparr>" inductive reachable where init: "reachable \<lparr>pc = (\<lambda>_. assign_x), x = init_x, y = init_y\<rparr>" | x_step: "reachable (update_x (update_pc st i assign_y) i 1)" if "reachable st" "pc st i = assign_x" | y_step: "reachable (update_y (update_pc st i finished) i (x st ((i + 1) mod N)))" if "reachable st" "pc st i = assign_y" definition safe where "safe st \<equiv> (\<forall>i. Proc i \<longrightarrow> pc st i = finished) \<longrightarrow> (\<exists>i. Proc i \<and> y st i = 1)" end

theory Template imports Defs begin theorem reachable_safe : "safe st" if "reachable st" sorry end

theory Check imports Submission begin theorem reachable_safe : "safe st" if "reachable st" using that by (rule Submission.reachable_safe) end

Download Files
### Definitions File

### Template File

### Check File

import tactic data.zmod.basic /- This is a specification of a simple concurrent algorithm from the paper "Teaching Concurrency" by Leslie Lamport. In there are N processes and two arrays of length N, x and y. Each process i executes the following sequence of statements: x[i] := 1; y[i] := x[(i-1) mod N]; The reads and writes of each x[j] are assumed to be atomic. This algorithm has the property that once all processes have finished, at least one y[j] == 1. -/ namespace concurrency /- N is the number of processes. -/ -- variable (N : ℕ) /- Processes are identified by natural numbers. A variable is a function over all natural numbers, not just those from [0, N). However, the definition of reachable below restricts updates to processes from [0, N) -/ def var (t) := ℕ → t /- There's at least one process. -/ -- variable [fact (0 < N)] /- Control state of a process. A process is at control state assign_x if it has not started, assign_y if it has executed its assignment to x but not to y, and done if it has finished. -/ inductive pc_label | assign_x | assign_y | finished open pc_label /- State of the system. -/ structure state := (pc : var pc_label) (x : var nat) (y : var nat) def update {α} (i x) (v : var α) : var α | j := if i = j then x else v j @[simp] def update_pc (st : state) (i l) : state := { pc := update i l st.pc .. st } @[simp] def update_x (st : state) (i v) : state := { x := update i v st.x .. st } @[simp] def update_y (st : state) (i v) : state := { y := update i v st.y .. st } inductive reachable : state → Prop | init (init_x init_y : var nat) : reachable { pc := (λ _, assign_x), x := init_x, y := init_y } | x_step (st i) : reachable st → st.pc i = assign_x → reachable (update_x (update_pc st i assign_y) i 1) | y_step (st i) : reachable st → st.pc i = assign_y → reachable (update_y (update_pc st i finished) i (st.x (i+1))) def safe (st : state) := (∀ i, st.pc i = finished) → (∃ i, st.y i = 1) ----------------------just some definitions to prevent cheating------------------------ def reachable_safe_prop : Prop := ∀ (st : state) (h : reachable st), safe st notation `reachable_safe_prop` := reachable_safe_prop end concurrency

import .defs namespace concurrency theorem reachable_safe : ∀ (st : state) (h : reachable st), safe st := sorry end concurrency

import .defs import .submission lemma check_reachable_safe : reachable_safe_prop := @concurrency.reachable_safe

Download Files
### Definitions File

### Template File

Require Export Coq.Arith.PeanoNat. Section Problem. (* N is the number of processes. *) Parameter N : nat. (* Processes are identified by natural numbers. A variable is a function over all natural numbers, not just those from [0, N). However, the definition of reachable below restricts updates to processes from [0, N) *) Definition var (T : Set) := nat -> T. Definition Proc (i : nat) := i < N. (* There's at least one process. *) Axiom Proc_0 : Proc 0. (* Control state of a process. A process is at control state assign_x if it has not started, assign_y if it has executed its assignment to x but not to y, and done if it has finished. *) Inductive pc_label := | assign_x | assign_y | done. (* State of the system. *) Record state : Set := mkState { pc : var pc_label ; x : var nat ; y : var nat }. (* Update the pc value of a single process *) Definition update_pc (st : state) (i : nat) (l : pc_label) : state := {|pc := fun j => if Nat.eq_dec i j then l else st.(pc) j ; x := st.(x) ; y := st.(y)|}. (* Update the x value of a single process *) Definition update_x (st : state) (i : nat) (v : nat) : state := {|pc := st.(pc) ; x := fun j => if Nat.eq_dec i j then v else st.(x) j ; y := st.(y)|}. (* Update the y value of a single process *) Definition update_y (st : state) (i : nat) (v : nat) : state := {|pc := st.(pc) ; x := st.(x) ; y := fun j => if Nat.eq_dec i j then v else st.(y) j|}. (* Set of reachable states *) Inductive reachable : state -> Prop := | init : forall init_x init_y, reachable {|pc := fun _ => assign_x; x := init_x; y := init_y |} | x_step : forall st, reachable st -> forall i, Proc i -> st.(pc) i = assign_x -> reachable (update_x (update_pc st i assign_y) i 1) | y_step : forall st, reachable st -> forall i, Proc i -> st.(pc) i = assign_y -> let j := if Nat.eq_dec (i + 1) N then 0 else i + 1 in reachable (update_y (update_pc st i done) i (st.(x) j)) . (* Property we want to prove: if every process is done, at least one process has y[i] = 1. *) Definition safe st := (forall i, Proc i -> st.(pc) i = done) -> exists i, Proc i /\ st.(y) i = 1. End Problem.

Require Import Defs. Theorem reachable_safe st: reachable st -> safe st. Proof. Admitted.

Terms and Conditions