Skip to content

Commit 5357dca

Browse files
lyrmlyrm
committed
Apply ocamlformat.
1 parent f0a8bd5 commit 5357dca

File tree

2 files changed

+76
-70
lines changed

2 files changed

+76
-70
lines changed

‎test/dune‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@
2222
(name stm_ws_deque)
2323
(modules stm_ws_deque)
2424
(libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
25-
(action (run %{test} --verbose)))
25+
(action
26+
(run %{test} --verbose)))
2627

2728
(test
2829
(name qcheck_mpsc_queue)

‎test/stm_ws_deque.ml‎

Lines changed: 74 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,11 @@ open STM
55
open Util
66
module Ws_deque = Lockfree.Ws_deque
77

8-
module WSDConf =
9-
struct
10-
type cmd =
11-
| Push of int
12-
| Pop
13-
| Steal
14-
15-
let show_cmd c = match c with
8+
module WSDConf = struct
9+
type cmd = Push of int | Pop | Steal
10+
11+
let show_cmd c =
12+
match c with
1613
| Push i -> "Push " ^ string_of_int i
1714
| Pop -> "Pop"
1815
| Steal -> "Steal"
@@ -24,90 +21,98 @@ struct
2421
let int_gen = Gen.nat in
2522
QCheck.make ~print:show_cmd
2623
(Gen.oneof
27-
[Gen.map (fun i -> Push i) int_gen;
28-
Gen.return Pop;
29-
(*Gen.return Steal;*) (* No point in stealing from yourself :-D *)
24+
[
25+
Gen.map (fun i -> Push i) int_gen;
26+
Gen.return Pop;
27+
(*Gen.return Steal;*)
28+
(* No point in stealing from yourself :-D *)
3029
])
31-
let stealer_cmd _s =
32-
QCheck.make ~print:show_cmd (Gen.return Steal)
3330

34-
let init_state = []
31+
let stealer_cmd _s = QCheck.make ~print:show_cmd (Gen.return Steal)
32+
let init_state = []
3533
let init_sut () = Ws_deque.M.create ()
36-
let cleanup _ = ()
34+
let cleanup _ = ()
3735

38-
let next_state c s = match c with
39-
| Push i -> i::s (*if i<>1213 then i::s else s*) (* an artificial fault *)
40-
| Pop -> (match s with
41-
| [] -> s
42-
| _::s' -> s')
43-
| Steal -> (match List.rev s with
44-
| [] -> s
45-
| _::s' -> List.rev s')
36+
let next_state c s =
37+
match c with
38+
| Push i ->
39+
i :: s
40+
(*if i<>1213 then i::s else s*)
41+
(* an artificial fault *)
42+
| Pop -> ( match s with [] -> s | _ :: s' -> s')
43+
| Steal -> ( match List.rev s with [] -> s | _ :: s' -> List.rev s')
4644

4745
let precond _ _ = true
4846

49-
let run c d = match c with
50-
| Push i -> Res (unit, Ws_deque.M.push d i)
51-
| Pop -> Res (result int exn, protect Ws_deque.M.pop d)
52-
| Steal -> Res (result int exn, protect Ws_deque.M.steal d)
53-
54-
let postcond c (s : state) res = match c,res with
55-
| Push _, Res ((Unit,_),_) -> true
56-
| Pop, Res ((Result (Int,Exn),_),res) ->
57-
(match s with
58-
| [] -> res = Error Exit
59-
| j::_ -> res = Ok j)
60-
| Steal, Res ((Result (Int,Exn),_),res) ->
61-
(match List.rev s with
62-
| [] -> Result.is_error res
63-
| j::_ -> res = Ok j)
64-
| _,_ -> false
47+
let run c d =
48+
match c with
49+
| Push i -> Res (unit, Ws_deque.M.push d i)
50+
| Pop -> Res (result int exn, protect Ws_deque.M.pop d)
51+
| Steal -> Res (result int exn, protect Ws_deque.M.steal d)
52+
53+
let postcond c (s : state) res =
54+
match (c, res) with
55+
| Push _, Res ((Unit, _), _) -> true
56+
| Pop, Res ((Result (Int, Exn), _), res) -> (
57+
match s with [] -> res = Error Exit | j :: _ -> res = Ok j)
58+
| Steal, Res ((Result (Int, Exn), _), res) -> (
59+
match List.rev s with [] -> Result.is_error res | j :: _ -> res = Ok j)
60+
| _, _ -> false
6561
end
6662

67-
module WSDT_seq = STM_sequential.Make(WSDConf)
68-
module WSDT_dom = STM_domain.Make(WSDConf)
63+
module WSDT_seq = STM_sequential.Make (WSDConf)
64+
module WSDT_dom = STM_domain.Make (WSDConf)
6965

7066
(* The following definitions differ slightly from those in multicoretests:lib/STM.ml.
7167
This has to do with how work-stealing deques are supposed to be used according to spec:
7268
- [agree_prop_par] differs in that it only spawns one domain ("a stealer domain")
7369
in parallel with the original "owner domain" (it also uses [Semaphore.Binary]) *)
74-
let agree_prop_par =
75-
(fun (seq_pref,owner,stealer) ->
76-
assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@owner));
77-
assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref@stealer));
78-
let sut = WSDConf.init_sut () in
79-
let pref_obs = WSDT_dom.interp_sut_res sut seq_pref in
80-
let sema = Semaphore.Binary.make false in
81-
let stealer_dom = Domain.spawn (fun () -> Semaphore.Binary.release sema; WSDT_dom.interp_sut_res sut stealer) in
82-
while not (Semaphore.Binary.try_acquire sema) do Domain.cpu_relax() done;
83-
let own_obs = WSDT_dom.interp_sut_res sut owner in
84-
let stealer_obs = Domain.join stealer_dom in
85-
let res = WSDT_dom.check_obs pref_obs own_obs stealer_obs WSDConf.init_state in
86-
let () = WSDConf.cleanup sut in
87-
res ||
88-
Test.fail_reportf " Results incompatible with linearized model:\n\n%s"
89-
@@ Util.print_triple_vertical ~center_prefix:false STM.show_res
90-
(List.map snd pref_obs,
91-
List.map snd own_obs,
92-
List.map snd stealer_obs))
70+
let agree_prop_par (seq_pref, owner, stealer) =
71+
assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ owner));
72+
assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ stealer));
73+
let sut = WSDConf.init_sut () in
74+
let pref_obs = WSDT_dom.interp_sut_res sut seq_pref in
75+
let sema = Semaphore.Binary.make false in
76+
let stealer_dom =
77+
Domain.spawn (fun () ->
78+
Semaphore.Binary.release sema;
79+
WSDT_dom.interp_sut_res sut stealer)
80+
in
81+
while not (Semaphore.Binary.try_acquire sema) do
82+
Domain.cpu_relax ()
83+
done;
84+
let own_obs = WSDT_dom.interp_sut_res sut owner in
85+
let stealer_obs = Domain.join stealer_dom in
86+
let res =
87+
WSDT_dom.check_obs pref_obs own_obs stealer_obs WSDConf.init_state
88+
in
89+
let () = WSDConf.cleanup sut in
90+
res
91+
|| Test.fail_reportf " Results incompatible with linearized model:\n\n%s"
92+
@@ Util.print_triple_vertical ~center_prefix:false STM.show_res
93+
(List.map snd pref_obs, List.map snd own_obs, List.map snd stealer_obs)
9394

9495
(* [arb_cmds_par] differs in what each triple component generates:
9596
"Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *)
96-
let arb_cmds_par = WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd
97+
let arb_cmds_par =
98+
WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd
9799

98100
(* A parallel agreement test - w/repeat and retries combined *)
99101
let agree_test_par ~count ~name =
100102
let rep_count = 50 in
101-
Test.make ~retries:10 ~count ~name
102-
arb_cmds_par (repeat rep_count agree_prop_par)
103+
Test.make ~retries:10 ~count ~name arb_cmds_par
104+
(repeat rep_count agree_prop_par)
103105

104106
(* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
105-
let agree_test_par_negative ~count ~name = WSDT_dom.neg_agree_test_par ~count ~name
107+
let agree_test_par_negative ~count ~name =
108+
WSDT_dom.neg_agree_test_par ~count ~name
106109

107110
let () =
108111
let count = 1000 in
109-
QCheck_base_runner.run_tests_main [
110-
WSDT_seq.agree_test ~count ~name:"STM Lockfree.Ws_deque test sequential";
111-
agree_test_par ~count ~name:"STM Lockfree.Ws_deque test parallel";
112-
agree_test_par_negative ~count ~name:"STM Lockfree.Ws_deque test parallel, negative";
113-
]
112+
QCheck_base_runner.run_tests_main
113+
[
114+
WSDT_seq.agree_test ~count ~name:"STM Lockfree.Ws_deque test sequential";
115+
agree_test_par ~count ~name:"STM Lockfree.Ws_deque test parallel";
116+
agree_test_par_negative ~count
117+
~name:"STM Lockfree.Ws_deque test parallel, negative";
118+
]

0 commit comments

Comments
 (0)