|
| 1 | +open QCheck |
| 2 | +open Domainslib |
| 3 | + |
| 4 | +(** This is a parallel test of Domainslib.Chan *) |
| 5 | + |
| 6 | +module ChConf = |
| 7 | +struct |
| 8 | + type state = int list |
| 9 | + type sut = int Domainslib.Chan.t |
| 10 | + type cmd = |
| 11 | + | Send of int |
| 12 | + | Send_poll of int |
| 13 | + | Recv |
| 14 | + | Recv_poll [@@deriving show { with_path = false }] |
| 15 | + |
| 16 | + let capacity = 8 |
| 17 | + |
| 18 | + let arb_cmd s = |
| 19 | + let int_gen = Gen.nat in |
| 20 | + QCheck.make ~print:show_cmd |
| 21 | + (if s=[] |
| 22 | + then |
| 23 | + Gen.oneof |
| 24 | + [Gen.map (fun i -> Send i) int_gen; |
| 25 | + Gen.map (fun i -> Send_poll i) int_gen; |
| 26 | + Gen.return Recv_poll] (* don't generate blocking Recv cmds on an empty channel *) |
| 27 | + else |
| 28 | + if List.length s >= capacity |
| 29 | + then |
| 30 | + Gen.oneof |
| 31 | + [Gen.map (fun i -> Send_poll i) int_gen; |
| 32 | + Gen.return Recv; |
| 33 | + Gen.return Recv_poll] (* don't generate blocking Send cmds on a full channel *) |
| 34 | + else |
| 35 | + Gen.oneof |
| 36 | + [Gen.map (fun i -> Send i) int_gen; |
| 37 | + Gen.map (fun i -> Send_poll i) int_gen; |
| 38 | + Gen.return Recv; |
| 39 | + Gen.return Recv_poll]) |
| 40 | + let init_state = [] |
| 41 | + let init_sut () = Chan.make_bounded capacity |
| 42 | + let cleanup _ = () |
| 43 | + |
| 44 | + let next_state c s = match c with |
| 45 | + | Send i -> if List.length s < capacity then s@[i] else s |
| 46 | + | Send_poll i -> if List.length s < capacity then s@[i] else s |
| 47 | + | Recv -> begin match s with [] -> [] | _::s' -> s' end |
| 48 | + | Recv_poll -> begin match s with [] -> [] | _::s' -> s' end |
| 49 | + |
| 50 | + let precond c s = match c,s with |
| 51 | + | Recv, [] -> false |
| 52 | + | Send _, _ -> List.length s < capacity |
| 53 | + | _, _ -> true |
| 54 | + |
| 55 | + type res = RSend | RSend_poll of bool | RRecv of int | RRecv_poll of int option [@@deriving show { with_path = false }] |
| 56 | + |
| 57 | + let run c chan = |
| 58 | + match c with |
| 59 | + | Send i -> (Chan.send chan i; RSend) |
| 60 | + | Send_poll i -> RSend_poll (Chan.send_poll chan i) |
| 61 | + | Recv -> RRecv (Chan.recv chan) |
| 62 | + | Recv_poll -> RRecv_poll (Chan.recv_poll chan) |
| 63 | + |
| 64 | + let postcond c s res = match c,res with |
| 65 | + | Send _, RSend -> (List.length s < capacity) |
| 66 | + | Send_poll _, RSend_poll res -> res = (List.length s < capacity) |
| 67 | + | Recv, RRecv res -> (match s with [] -> false | res'::_ -> res=res') |
| 68 | + | Recv_poll, RRecv_poll opt -> (match s with [] -> None | res'::_ -> Some res') = opt |
| 69 | + | _,_ -> false |
| 70 | +end |
| 71 | + |
| 72 | + |
| 73 | +module ChT = STM.Make(ChConf) |
| 74 | +;; |
| 75 | +Util.set_ci_printing () |
| 76 | +;; |
| 77 | +QCheck_runner.run_tests_main |
| 78 | + (let count,name = 1000,"global Domainslib.Chan test" in [ |
| 79 | + ChT.agree_test ~count ~name; |
| 80 | + ChT.agree_test_par ~count ~name; |
| 81 | + ]) |
0 commit comments