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.

# Concurrency

This is a specification of a simple concurrent algorithm. In there, `N` concurrent processes access 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, there is at least one `j` with `y[j] == 1`. The template file contains a simple model of this algorithm. Your task is to prove that the system is "safe" at any point of its execution: Either, one process has not terminated yet, or at least one `j` has `y[j] == 1`. Submitted by: Daniel Ricketts Coq: Daniel Ricketts (& Fabian Kunze) | Lean: Simon Hudon & Kevin Kappelmann | Isabelle: Simon Wimmer

## Resources

### Definitions 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
```

### Template File

```theory Template
imports Defs
begin

theorem reachable_safe :
"safe st" if "reachable st"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem reachable_safe :
"safe st" if "reachable st"
using that by (rule Submission.reachable_safe)

end
```

### Definitions 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
```

### Template File

```import .defs

namespace concurrency

theorem reachable_safe : ∀ (st : state) (h : reachable st), safe st :=
sorry

end concurrency
```

### Check File

```import .defs
import .submission

lemma check_reachable_safe : reachable_safe_prop := @concurrency.reachable_safe
```

### Definitions 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.
```

### Template File

```Require Import Defs.

Theorem reachable_safe st:
reachable st -> safe st.
Proof.
```

### Definitions 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
```

### Template File

```theory Template
imports Defs
begin

theorem reachable_safe :
"safe st" if "reachable st"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem reachable_safe :
"safe st" if "reachable st"
using that by (rule Submission.reachable_safe)

end
```

Terms and Conditions