Cookies disclaimer

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.

[Proof Ground 2020] Concurrency

Resources

Download Files

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
Download Files

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
Download Files

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.
Admitted.
Download Files

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