1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
open Printf
(* Main mode *)
type mode = Explo | Conform
let parse_mode s = match Misc.lowercase s with
| "explo" -> Some Explo
| "conform" -> Some Conform
| _ -> None
let pp_mode = function
| Explo -> "explo"
| Conform -> "conform"
(* Execution *)
type mach =
| Local
| Distant of string
| Simul of string * string
| Cross of string * string
let split_space s =
try
let i = String.index s ' ' in
String.sub s 0 i,
String.sub s (i+1) (String.length s - (i+1))
with Not_found -> s,""
let parse_mach s =
let key,v = split_space s in
match Misc.lowercase key with
| "local" -> Some Local
| "ssh" -> Some (Distant v)
| ("memevents"|"ppcmem"|"herd") as prog ->
Some (Simul (prog,v))
| "cross" ->
let v1,v2 = split_space v in
Some (Cross (v1,v2))
| _ -> None
let sp s = if s = "" then "" else " "
let pp_mach = function
| Local -> "local"
| Distant addr -> sprintf "ssh %s" addr
| Simul (prog,opts) ->
sprintf "%s%s%s" prog (sp opts) opts
| Cross (addr1,addr2) -> sprintf "cross %s %s" addr1 addr2
(* Interpretation *)
type interpretation = Single | Multi
let parse_interpretation s = match Misc.lowercase s with
| "single" -> Some Single
| "multi" -> Some Multi
| _ -> None
let pp_interpretation = function
| Single -> "single"
| Multi -> "multi"
(* Checkpoint *)
let ckpt_name = "ckpt"
type t =
{
arch : Archs.t ;
output : string ; (* Directory for all output *)
testing : string option ;
safe : string option ;
mode : mode ;
mach : mach ;
interpretation : interpretation ;
work_dir : string ;
nprocs : int option ;
diy_sz : int option ;
litmus_opts : string ;
run_opts : string list ;
verbose : int ;
interactive : bool ;
force_interactive : bool ;
build : string ;
stabilise : int ;
compress : bool ;
distrm : string ;
distaddpath : string list ;
diy_opts : string list ;
transitive : bool ;
}
let pp_opt chan t =
let pp_opt pp = function
| None -> "-"
| Some x -> pp x in
let pp_oint = pp_opt string_of_int in
let p = fprintf chan in
p "arch = %s\n" (Archs.pp t.arch) ;
p "nprocs = %s\n" (pp_oint t.nprocs) ;
p "diy_sz = %s\n" (pp_oint t.diy_sz) ;
()
let default =
{
arch = `X86 ;
output = "." ;
testing = None ;
safe = None ;
mach = Local ;
mode = Explo ;
interpretation = Single ;
work_dir = "/var/tmp" ;
nprocs = None ;
diy_sz = None ;
litmus_opts = "" ;
run_opts = ["";] ;
verbose = 0 ;
interactive = true ;
force_interactive = false ;
build = "sh comp.sh" ;
stabilise = 5 ;
compress = true ;
distrm = "/bin/rm" ;
distaddpath = [] ;
diy_opts = [] ;
transitive = false ;
}
let incr_verbose opts = { opts with verbose = opts.verbose + 1 ; }
let set_interactive b opts = { opts with interactive = b ; }
let set_transitive b opts = { opts with transitive = b ; }
let set_compress b opts = { opts with compress = b ; }
let set_arch arg cfg = match Archs.parse arg with
| None -> raise (Arg.Bad (sprintf "unknown architecture: %s" arg))
| Some a -> { cfg with arch =a; }
let set_mode arg cfg = match parse_mode arg with
| None -> raise (Arg.Bad (sprintf "bad mode: %s" arg))
| Some m -> { cfg with mode = m ; }
let set_nprocs i cfg = { cfg with nprocs = Some i; }
let get_nprocs a cfg = match cfg.nprocs with
| None ->
begin
match a with
| `PPC -> 4
| `X86|`X86_64
| `ARM
| `MIPS
| `LISA
| `AArch64
| `RISCV -> 2
| `C | `CPP -> 2
end
| Some i -> i
let set_diy_opts s t = { t with diy_opts = s :: t.diy_opts; }
let get_diy_opts t = t.diy_opts
|
