m_prod_cons_futex.ml

open Printf
open Ddsv

type shared_vars = {
    mutex : int;
    cv_bits : int;
    cv_state : int;
    cv_old : int list;
    count : int;
}

let max_count = 1
let num_producers = 1
let num_consumers = 1
let num_processes = num_producers + num_consumers

let rec interval a b =
  if a >= b then
    []
  else
    a::(interval (a+1) b)

let r0 = { mutex = 0; cv_bits = 0; cv_state = 0;
           cv_old = List.map (fun k -> 0) (interval 0 num_processes);
           count = 0 }

let show_list xs =
  let s =
    List.fold_left
      (fun s k -> sprintf "%s %d" s k)
    "[" xs
  in s ^ " ]"

let show_sv r =
  sprintf "m=%d cvb=%x cvs=%d cvo=%s cnt=%d"
    r.mutex r.cv_bits r.cv_state (show_list r.cv_old) r.count

let rec list_update xs k y =
  match xs with
    [] -> raise Not_found
  | x::xs' ->
     if k=0 then
       y::xs'
     else
       x::(list_update xs' (k-1) y)

let signal r =
  { r with cv_bits = r.cv_bits land (r.cv_bits - 1) }

let producer i = [
    ("P0", [("P.lock", "P1", (fun r -> r.mutex = 0),
             (fun r -> { r with mutex = 1 }))]);
    ("P1", [("P.save", "P2", (fun r -> r.count = max_count), (* full *)
             (fun r -> { r with cv_old = list_update r.cv_old i r.cv_state }));
            ("P.produce", "P5", (fun r -> r.count < max_count),
             (fun r -> { r with count = r.count + 1 })) ]);
    ("P2", [("P.unlock", "P3", (fun r -> true),
             (fun r -> { r with mutex = 0 }))]);
    ("P3", [("P.futex_wait", "P4", (fun r -> r.cv_state = List.nth r.cv_old i),
             (fun r -> { r with cv_bits = r.cv_bits lor (1 lsl i);
                                cv_old = list_update r.cv_old i 0})); (* RST *)
            ("P.futex_miss", "P0", (fun r -> r.cv_state <> List.nth r.cv_old i),
             (fun r -> { r with cv_old = list_update r.cv_old i 0 }))]);
    ("P4", [("P.wakeup", "P0", (fun r -> r.cv_bits land (1 lsl i) = 0),
             (fun r -> r))]);
    ("P5", [("P.inc", "P6", (fun r -> true),
             (fun r -> { r with cv_state = (r.cv_state + 1) mod (num_processes + 1)}))]);
    ("P6", [("P.futex_wake", "P7", (fun r -> true), signal)]);
    ("P7", [("P.unlock", "P0", (fun r -> true),
             (fun r -> { r with mutex = 0 }))]);
  ]


let consumer i = [
    ("Q0", [("Q.lock", "Q1", (fun r -> r.mutex = 0),
             (fun r -> { r with mutex = 1 }))]);
    ("Q1", [("Q.save", "Q2", (fun r -> r.count = 0),
             (fun r -> { r with cv_old = list_update r.cv_old i r.cv_state }));
            ("Q.consume", "Q5", (fun r -> r.count > 0),
             (fun r -> { r with count = r.count - 1 })) ]);
    ("Q2", [("Q.unlock", "Q3", (fun r -> true),
             (fun r -> { r with mutex = 0 }))]);
    ("Q3", [("Q.futex_wait", "Q4", (fun r -> r.cv_state = List.nth r.cv_old i),
             (fun r -> { r with cv_bits = r.cv_bits lor (1 lsl i);
                                cv_old = list_update r.cv_old i 0})); (* RST *)
            ("Q.futex_miss", "Q0", (fun r -> r.cv_state <> List.nth r.cv_old i),
             (fun r -> { r with cv_old = list_update r.cv_old i 0 }))]);
    ("Q4", [("Q.wakeup", "Q0", (fun r -> r.cv_bits land (1 lsl i) = 0),
             (fun r -> r))]);
    ("Q5", [("Q.inc", "Q6", (fun r -> true),
             (fun r -> { r with cv_state = (r.cv_state + 1) mod (num_processes + 1)}))]);
    ("Q6", [("Q.futex_wake", "Q7", (fun r -> true), signal)]);
    ("Q7", [("Q.unlock", "Q0", (fun r -> true),
             (fun r -> { r with mutex = 0 }))]);
  ]

let ps =
  (List.map (fun k -> producer k) (interval 0 num_producers)) @
  (List.map (fun k -> consumer k) (interval num_producers num_processes))

let () =
  viz_process "m_prod_cons_futex_P" (producer 0);
  viz_process "m_prod_cons_futex_Q" (consumer 1);
  let lts = concurrent_composition r0 ps in
  lts_print_deadlocks stdout show_sv lts;
  viz_lts "m_prod_cons_futex" show_sv lts