Skip to content

Commit

Permalink
add seed, add generate cas, fad
Browse files Browse the repository at this point in the history
  • Loading branch information
@bartoszmodelski
bartoszmodelski committed Apr 24, 2023
1 parent 63a414d commit 890e668
Showing 1 changed file with 91 additions and 25 deletions.
116 changes: 91 additions & 25 deletions tests/gen_program.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ type config = {
thread_count : int;
generate_conditionals : bool;
print_tests : bool;
seed : int option;
}

let print_config t =
Expand All @@ -16,29 +17,60 @@ let print_config t =
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
Printf.printf "generate_conditionals: %b\n%!" t.generate_conditionals;
Printf.printf "seed: %s\n%!"
(Option.map Int.to_string t.seed |> Option.value ~default:"<random>")

let var_name i = Char.chr (i + 97)

module Function = struct
(* Arbitrary function from int to bool *)
type t = IntSet.t
type t =
| Get of { true_on : IntSet.t }
| CompareAndSet of { old_value : int; new_value : int }
| FetchAndAdd of { delta : int; true_on : IntSet.t }

let rec gen value_limit =
let true_set =
List.init value_limit (fun i -> if Random.bool () then Some i else None)
|> List.filter_map Fun.id |> IntSet.of_list
let gen value_limit =
let rec set_f () =
let set =
List.init value_limit (fun i -> if Random.bool () then Some i else None)
|> List.filter_map Fun.id |> IntSet.of_list
in
let size = IntSet.cardinal set in
if 0 < size && size < value_limit then set else set_f ()
in
let size = IntSet.cardinal true_set in
if 0 < size && size < value_limit then true_set else gen value_limit
match Random.int 6 with
| 0 | 1 | 2 -> Get { true_on = set_f () }
| 3 | 4 ->
let old_value = Random.int value_limit in
let new_value = Random.int value_limit in
CompareAndSet { old_value; new_value }
| 5 ->
let delta = Random.int value_limit in
FetchAndAdd { delta; true_on = set_f () }
| _ -> assert false

let eval t input = IntSet.mem input t
let eval variable = function
| Get { true_on } -> IntSet.mem (Atomic.get variable) true_on
| FetchAndAdd { delta; true_on } ->
IntSet.mem (Atomic.fetch_and_add variable delta) true_on
| CompareAndSet { old_value; new_value } ->
Atomic.compare_and_set variable old_value new_value

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 "; ")
let to_string var_id = function
| Get { true_on } ->
Printf.sprintf "IntSet.mem (Atomic.get %c) (IntSet.of_list [%s])"
(var_name var_id)
(IntSet.to_seq true_on |> List.of_seq |> List.map Int.to_string
|> String.concat "; ")
| FetchAndAdd { delta; true_on } ->
Printf.sprintf
"IntSet.mem (Atomic.fetch_and_add %c %d) (IntSet.of_list [%s])"
(var_name var_id) delta
(IntSet.to_seq true_on |> List.of_seq |> List.map Int.to_string
|> String.concat "; ")
| CompareAndSet { old_value; new_value } ->
Printf.sprintf "Atomic.compare_and_set %c %d %d" (var_name var_id)
old_value new_value
end

module Conditional = struct
Expand All @@ -57,8 +89,7 @@ module Conditional = struct
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
let output = Function.eval var func in
match (operator, output) with
| `Or, true -> true
| `And, false -> false
Expand All @@ -73,14 +104,21 @@ module Conditional = struct
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)
|> List.map (fun (func, var_id) -> Function.to_string var_id func)
|> 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 }
| CompareAndSet of {
var_id : int;
old_value : int;
new_value : int;
next : t;
}
| FetchAndAdd of { var_id : int; delta : int; next : t }
| Conditional of {
var_ids : int list;
conditional : Conditional.t;
Expand All @@ -96,6 +134,15 @@ module Step = struct
| Read { var_id; next } ->
ignore (Atomic.get (CCVector.get globals var_id));
run ~globals next
| CompareAndSet { var_id; old_value; new_value; next } ->
ignore
(Atomic.compare_and_set
(CCVector.get globals var_id)
old_value new_value);
run ~globals next
| FetchAndAdd { var_id; delta; next } ->
ignore (Atomic.fetch_and_add (CCVector.get globals var_id) delta);
run ~globals next
| Conditional { var_ids; conditional; on_true; next } ->
let variables =
List.map (fun var_id -> CCVector.get globals var_id) var_ids
Expand All @@ -113,6 +160,14 @@ module Step = struct
| Read { var_id; next } ->
Printf.printf "%sAtomic.get %c |> ignore;\n" indent (var_name var_id);
print ~depth next
| CompareAndSet { var_id; old_value; new_value; next } ->
Printf.printf "%sAtomic.compare_and_set %c %d %d |> ignore;\n" indent
(var_name var_id) old_value new_value;
print ~depth next
| FetchAndAdd { var_id; delta; next } ->
Printf.printf "%sAtomic.fetch_and_add %c %d |> ignore;\n" indent
(var_name var_id) delta;
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;
Expand All @@ -127,12 +182,19 @@ module Step = struct
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 ->
match Random.int (6 + maybe_conditionals) with
| 0 | 1 ->
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 ->
| 2 | 3 -> Read { var_id; next = next fuel }
| 4 ->
let old_value = Random.int config.value_limit in
let new_value = Random.int config.value_limit in
CompareAndSet { var_id; old_value; new_value; next = next fuel }
| 5 ->
let delta = Random.int config.value_limit - (config.value_limit / 2) in
FetchAndAdd { var_id; delta; next = next fuel }
| 6 ->
let func_count =
min (max 1 fuel) (min config.globals_count (1 + Random.int 2))
in
Expand All @@ -144,7 +206,7 @@ module Step = struct
in
let fuel_a, fuel_b =
let tmp = Random.int (max (fuel - func_count) 1) in
(tmp/2, tmp/2)
(tmp / 2, tmp / 2)
in

let on_true = gen ~config ~fuel:fuel_a () in
Expand Down Expand Up @@ -179,13 +241,14 @@ module Program = struct
end

let run_random config () =
Random.self_init ();
(match config.seed with
| None -> Random.self_init ()
| Some seed -> Random.init seed);
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 (
Expand All @@ -212,6 +275,7 @@ let _ =
let thread_count = ref 3 in
let generate_conditionals = ref true in
let print_tests = ref false in
let seed = ref 0 in
let speclist =
[
( "-test-count",
Expand All @@ -232,6 +296,7 @@ let _ =
( "-generate-conditionals",
Arg.Set generate_conditionals,
"enable/disable generation of conditional statements" );
("-seed", Arg.Set_int seed, "random seed for generation");
]
in
Arg.parse speclist
Expand All @@ -247,6 +312,7 @@ let _ =
thread_count = !thread_count;
generate_conditionals = !generate_conditionals;
print_tests = !print_tests;
seed = (if !seed > 0 then Some !seed else None);
}
: config)
in
Expand Down

0 comments on commit 890e668

Please sign in to comment.