add program generation

Author: bartoszmodelski

src/trace_tracker.ml

@@ -104,3 +104,8 @@ let equal t1 t2 =
       (* any values under the same key are known to be equivalent, even if the exact sequence is not identical *))
     t1 t2
   == 0
+
+
+let subset t1 t2 = 
+  TraceMap.fold (fun key _ seen_all -> 
+    TraceMap.mem key t2 && seen_all) t1 true

src/trace_tracker.mli

@@ -7,3 +7,4 @@ val print_traces : out_channel -> unit
 val print : t -> out_channel -> unit
 val equal : t -> t -> bool
 val get_deps_str : t -> string
+val subset : t -> t -> bool

src/tracedAtomic.ml

@@ -310,6 +310,22 @@ let do_run init_func init_schedule =
         backtrack = IntSet.empty;
       }
 
+let rec explore_random func state =
+  let s = last_element state in
+  let enabled = IntSet.to_seq s.enabled |> List.of_seq in
+  let len = List.length enabled in
+  if len == 0 then ()
+  else
+    let random_index = Random.int (List.length enabled) in
+    let j = List.nth enabled random_index in
+    let j_proc = List.nth s.procs j in
+    let schedule =
+      List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state
+      @ [ (j, j_proc.op, j_proc.obj_ptr) ]
+    in
+    let statedash = state @ [ do_run func schedule ] in
+    explore_random func statedash
+
 let rec explore func state clock last_access =
   let s = last_element state in
   List.iter
@@ -371,18 +387,25 @@ let reset_state () =
 
 let dscheck_trace_file_env = Sys.getenv_opt "dscheck_trace_file"
 
+let random func iters =
+  reset_state ();
+  let empty_state = do_run func [ (0, Start, None) ] :: [] in
+  for _ = 1 to iters do
+    explore_random func empty_state
+  done
+
 let dpor func =
   reset_state ();
   let empty_state = do_run func [ (0, Start, None) ] :: [] in
   let empty_clock = IntMap.empty in
   let empty_last_access = IntMap.empty in
   explore func empty_state empty_clock empty_last_access
 
-let trace ?interleavings ?(record_traces = false) func =
+let trace ?(impl = `Dpor) ?interleavings ?(record_traces = false) func =
   record_traces_flag := record_traces || Option.is_some dscheck_trace_file_env;
   interleavings_chan := interleavings;
 
-  dpor func;
+  (match impl with `Dpor -> dpor func | `Random iters -> random func iters);
 
   (* print reports *)
   (match !interleavings_chan with

src/tracedAtomic.mli

@@ -47,7 +47,11 @@ val decr : int t -> unit
 (** [decr r] atomically decrements the value of [r] by [1]. *)
 
 val trace :
-  ?interleavings:out_channel -> ?record_traces:bool -> (unit -> unit) -> unit
+  ?impl:[ `Random of int | `Dpor ] ->
+  ?interleavings:out_channel ->
+  ?record_traces:bool ->
+  (unit -> unit) ->
+  unit
 (** start the simulation trace *)
 
 val spawn : (unit -> unit) -> unit

tests/dune

@@ -37,3 +37,8 @@
  (name test_conditional2)
  (libraries dscheck alcotest)
  (modules test_conditional2))
+
+(executable
+ (name gen_program)
+ (libraries dscheck)
+ (modules gen_program))

tests/gen_program.ml

@@ -0,0 +1,251 @@
+module Atomic = Dscheck.TracedAtomic
+module IntSet = Set.Make (Int)
+
+type config = {
+  globals_count : int;
+  value_limit : int;
+  operations_count : int;
+  thread_count : int;
+  generate_conditionals : bool;
+  print_tests : bool;
+}
+
+let print_config t =
+  Printf.printf "CONFIG\n";
+  Printf.printf "globals_count: %d\n" t.globals_count;
+  Printf.printf "value_limit: %d\n" t.value_limit;
+  Printf.printf "operations_count: %d\n" t.operations_count;
+  Printf.printf "thread_count: %d\n" t.thread_count;
+  Printf.printf "generate_conditionals: %b\n%!" t.generate_conditionals
+
+let var_name i = Char.chr (i + 97)
+
+module Function = struct
+  (* Arbitrary function from int to bool *)
+  type t = IntSet.t
+
+  let gen value_limit =
+    List.init value_limit (fun i -> if Random.bool () then Some i else None)
+    |> List.filter_map Fun.id |> IntSet.of_list
+
+  let eval t input = IntSet.mem input t
+
+  let to_string t var_id =
+    Printf.sprintf "IntSet.mem (Atomic.get %c) (IntSet.of_list [%s])"
+      (var_name var_id)
+      (IntSet.to_seq t |> List.of_seq |> List.map Int.to_string
+     |> String.concat "; ")
+end
+
+module Conditional = struct
+  type t = { functions : Function.t list; operator : [ `And | `Or ] }
+
+  let gen function_count ~value_limit =
+    let functions =
+      List.init function_count (fun _ -> Function.gen value_limit)
+    in
+    let operator = if Random.bool () then `And else `Or in
+    { functions; operator }
+
+  let eval t variables =
+    let functions = t.functions in
+    let rec f operator vars funcs =
+      match (vars, funcs) with
+      | [], [] -> ( match operator with `And -> true | `Or -> false)
+      | var :: vars_tl, func :: funcs_tl -> (
+          let input = Atomic.get var in
+          let output = Function.eval func input in
+          match (operator, output) with
+          | `Or, true -> true
+          | `And, false -> false
+          | `Or, false | `And, true -> f operator vars_tl funcs_tl)
+      | _, [] | [], _ ->
+          failwith
+            "gen_program: lists of variables and functions have different \
+             lengths"
+    in
+    f t.operator variables functions
+
+  let to_string t ~var_ids =
+    let operator_str = match t.operator with `Or -> " || " | `And -> " && " in
+    List.combine t.functions var_ids
+    |> List.map (fun (func, var_id) -> Function.to_string func var_id)
+    |> String.concat operator_str
+end
+
+module Step = struct
+  type t =
+    | Write of { var_id : int; new_value : int; next : t }
+    | Read of { var_id : int; next : t }
+    | Conditional of {
+        var_ids : int list;
+        conditional : Conditional.t;
+        on_true : t;
+        next : t;
+      }
+    | Noop
+
+  let rec run ~globals = function
+    | Write { var_id; new_value; next } ->
+        Atomic.set (CCVector.get globals var_id) new_value;
+        run ~globals next
+    | Read { var_id; next } ->
+        ignore (Atomic.get (CCVector.get globals var_id));
+        run ~globals next
+    | Conditional { var_ids; conditional; on_true; next } ->
+        let variables =
+          List.map (fun var_id -> CCVector.get globals var_id) var_ids
+        in
+        if Conditional.eval conditional variables then run ~globals on_true;
+        run ~globals next
+    | Noop -> ()
+
+  let rec print t ~depth =
+    let indent = List.init depth (fun _ -> "\t") |> String.concat "" in
+    match t with
+    | Write { var_id; new_value; next } ->
+        Printf.printf "%sAtomic.set %c %d;\n" indent (var_name var_id) new_value;
+        print ~depth next
+    | Read { var_id; next } ->
+        Printf.printf "%sAtomic.get %c |> ignore;\n" indent (var_name var_id);
+        print ~depth next
+    | Conditional { var_ids; conditional; on_true; next } ->
+        let s = Conditional.to_string conditional ~var_ids in
+        Printf.printf "%sif (%s) then (\n" indent s;
+        print ~depth:(depth + 1) on_true;
+        Printf.printf "%s);\n" indent;
+        print ~depth next
+    | Noop -> ()
+
+  let rec gen ~config ~fuel () =
+    let var_id = Random.int config.globals_count in
+    let next fuel =
+      if fuel > 1 then gen ~config ~fuel:(fuel - 1) () else Noop
+    in
+    let maybe_conditionals = if config.generate_conditionals then 1 else 0 in
+    match Random.int (2 + maybe_conditionals) with
+    | 0 ->
+        let new_value = Random.int config.value_limit in
+        Write { var_id; new_value; next = next fuel }
+    | 1 -> Read { var_id; next = next fuel }
+    | 2 ->
+        let func_count =
+          min (max 1 fuel) (min config.globals_count (1 + Random.int 2))
+        in
+        let var_ids =
+          List.init func_count (fun _ -> Random.int config.globals_count)
+        in
+        let conditional =
+          Conditional.gen func_count ~value_limit:config.value_limit
+        in
+        let fuel_a, fuel_b =
+          let tmp = Random.int (max (fuel - func_count) 1) in
+          (fuel - tmp, tmp)
+        in
+
+        let on_true = gen ~config ~fuel:fuel_a () in
+        Conditional { var_ids; conditional; on_true; next = next fuel_b }
+    | _ -> failwith "drew number without corresponding instruction"
+end
+
+module Program = struct
+  type thread = Step.t
+  type t = { globals : (int, CCVector.ro) CCVector.t; threads : thread list }
+
+  let run ~impl { globals; threads } =
+    Atomic.trace ~impl ~record_traces:true (fun () ->
+        let globals = CCVector.map Atomic.make globals |> CCVector.freeze in
+        List.iter
+          (fun thread -> Atomic.spawn (fun () -> Step.run ~globals thread))
+          threads;
+        ());
+    Dscheck.Trace_tracker.get_traces ()
+
+  let print { globals; threads } =
+    CCVector.iteri
+      (fun var_id value ->
+        Printf.printf "let %c = Atomic.make %d in\n" (var_name var_id) value)
+      globals;
+    List.iter
+      (fun thread ->
+        Printf.printf "\nDomain.spawn (fun () -> \n";
+        Step.print thread ~depth:1;
+        Printf.printf ")\n%!")
+      threads
+end
+
+let run_random config () =
+  Random.self_init ();
+  let globals = CCVector.of_list (List.init config.globals_count Fun.id) in
+  let thread_f = Step.gen ~config ~fuel:config.operations_count in
+  let threads = List.init config.thread_count (fun _ -> thread_f ()) in
+  let program = ({ globals; threads } : Program.t) in
+  if config.print_tests then 
+    Program.print program;
+
+  let random = Program.run ~impl:(`Random 100) program in
+  let dpor = Program.run ~impl:`Dpor program in
+  if not (Dscheck.Trace_tracker.subset random dpor) then (
+    Printf.printf "found mismatch\n\n%!";
+    Program.print program;
+    Dscheck.Trace_tracker.print dpor stdout;
+    Dscheck.Trace_tracker.print random stdout;
+    assert false)
+
+let run config test_count =
+  Printf.printf "\n\n";
+  for i = 0 to test_count do
+    Printf.printf "----run: %d/%d\r%!" i test_count;
+    run_random config ()
+  done;
+  Printf.printf "\nall generated programs passed\n%!"
+
+(* cmd *)
+let _ =
+  let test_count = ref 100 in
+  let globals_count = ref 6 in
+  let value_limit = ref 5 in
+  let operations_count = ref 3 in
+  let thread_count = ref 3 in
+  let generate_conditionals = ref true in
+  let print_tests = ref false in
+  let speclist =
+    [
+      ( "-test-count",
+        Arg.Set_int test_count,
+        "number of programs to generate and test" );
+        ("-print-tests", Arg.Set print_tests, "print all tests");
+      ( "-global-vars-count",
+        Arg.Set_int globals_count,
+        "number of shared atomic variables (the more, the higher the reduction)"
+      );
+      ( "-value-limit",
+        Arg.Set_int value_limit,
+        "range of values used by generated operations" );
+      ( "-operations-count",
+        Arg.Set_int operations_count,
+        "number of operations per thread" );
+      ("-thread-count", Arg.Set_int thread_count, "number of threads");
+      ( "-generate-conditionals",
+        Arg.Set generate_conditionals,
+        "enable/disable generation of conditional statements" );
+    ]
+  in
+  Arg.parse speclist
+    (fun _ -> ())
+    "gen_program.exe [-test-count INT] [-global-vars-count INT] [-value-limit \
+     INT] [-operations-count INT] [-thread-count INT] [-generate-conditionals \
+     BOOL]";
+  let config =
+    ({
+       globals_count = !globals_count;
+       value_limit = !value_limit;
+       operations_count = !operations_count;
+       thread_count = !thread_count;
+       generate_conditionals = !generate_conditionals;
+       print_tests = !print_tests
+     }
+      : config)
+  in
+  print_config config;
+  run config !test_count