Skip to content

Commit 2a1bc72

Browse files
LysxiaLysxia
authored
Use number of cores as default parallelism (#2236)
2 parents 64f0469 + 5538665 commit 2a1bc72

72 files changed

Lines changed: 454 additions & 294 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Cargo.lock‎

Lines changed: 17 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎cargo-creusot/src/why3find_wrapper.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,9 @@ pub struct ProveArgs {
3333
/// Print the Why3find command without running it.
3434
#[clap(long)]
3535
pub dry_run_why3find: bool,
36+
/// Max parallel provers
37+
#[clap(short = 'j')]
38+
pub jobs: Option<usize>,
3639
/// Run why3find on files that match one of the patterns.
3740
/// Examples: `name`, `name::*`, `m/*/f`, or whole paths `verif/a/b.coma`.
3841
pub patterns: Vec<String>,
@@ -67,7 +70,8 @@ fn check_why3find_json_exists(root: &Path) -> Result<()> {
6770
fn raw_prove(args: ProveArgs, paths: &CreusotPaths, files: &[PathBuf]) -> Result<()> {
6871
let mut why3find = Command::new(&paths.why3find());
6972
why3find.arg("prove");
70-
why3find.args(["-j", &format!("{}", creusot_setup::default_provers_parallelism())]);
73+
let jobs = args.jobs.unwrap_or_else(creusot_setup::default_provers_parallelism);
74+
why3find.args(["-j", &format!("{}", jobs)]);
7175
if args.ide.ide_on_fail {
7276
why3find.arg("-i");
7377
}

‎creusot-setup/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,4 @@ toml = { version = "0.9", features = ["preserve_order"] }
1111
directories = "6.0"
1212
which = "8.0"
1313
anyhow = "1.0"
14+
num_cpus = "1.17.0"

‎creusot-setup/src/lib.rs‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -139,8 +139,5 @@ timelimit = 5.000000
139139
}
140140

141141
pub fn default_provers_parallelism() -> usize {
142-
match std::thread::available_parallelism() {
143-
Ok(n) => n.get(),
144-
Err(_) => 1,
145-
}
142+
num_cpus::get_physical()
146143
}

‎examples/bdd/proof.json‎

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@
3737
"children": [
3838
{ "prover": "z3", "time": 0.02 },
3939
{ "prover": "alt-ergo", "time": 0.025 },
40-
{ "prover": "z3", "time": 0.151 },
40+
{ "prover": "z3", "time": 0.246 },
4141
{ "prover": "alt-ergo", "time": 0.047 },
4242
{ "prover": "z3", "time": 0.065 },
4343
{ "prover": "alt-ergo", "time": 0.053 },
@@ -89,32 +89,32 @@
8989
]
9090
},
9191
{ "prover": "z3", "time": 0.286 },
92-
{ "prover": "z3", "time": 0.183 },
92+
{ "prover": "z3", "time": 0.265 },
9393
{ "prover": "z3", "time": 0.037 },
9494
{ "prover": "z3", "time": 0.103 },
9595
{ "prover": "z3", "time": 0.04 },
9696
{
9797
"tactic": "split_vc",
9898
"children": [
99-
{ "prover": "alt-ergo", "time": 0.046 },
99+
{ "prover": "alt-ergo", "time": 0.24 },
100100
{ "prover": "alt-ergo", "time": 0.063 },
101-
{ "prover": "alt-ergo", "time": 0.056 }
101+
{ "prover": "alt-ergo", "time": 0.234 }
102102
]
103103
},
104104
{
105105
"tactic": "split_vc",
106106
"children": [
107107
{ "prover": "alt-ergo", "time": 0.054 },
108108
{ "prover": "alt-ergo", "time": 0.067 },
109-
{ "prover": "alt-ergo", "time": 0.065 }
109+
{ "prover": "alt-ergo", "time": 0.23 }
110110
]
111111
},
112112
{
113113
"tactic": "split_vc",
114114
"children": [
115-
{ "prover": "alt-ergo", "time": 0.074 },
116-
{ "prover": "alt-ergo", "time": 0.066 },
117-
{ "prover": "alt-ergo", "time": 0.067 }
115+
{ "prover": "alt-ergo", "time": 0.233 },
116+
{ "prover": "z3", "time": 0.057 },
117+
{ "prover": "z3", "time": 0.053 }
118118
]
119119
},
120120
{
@@ -131,16 +131,16 @@
131131
{ "prover": "alt-ergo", "time": 0.041 },
132132
{ "prover": "z3", "time": 0.064 },
133133
{ "prover": "z3", "time": 0.039 },
134-
{ "prover": "z3", "time": 0.175 },
134+
{ "prover": "z3", "time": 0.283 },
135135
{
136136
"tactic": "split_vc",
137137
"children": [
138138
{ "prover": "z3", "time": 0.059 },
139139
{
140140
"tactic": "split_vc",
141141
"children": [
142-
{ "prover": "alt-ergo", "time": 0.07 },
143-
{ "prover": "alt-ergo", "time": 0.123 },
142+
{ "prover": "alt-ergo", "time": 0.249 },
143+
{ "prover": "z3", "time": 0.036 },
144144
{ "prover": "z3", "time": 0.063 },
145145
{ "prover": "z3", "time": 0.033 }
146146
]
@@ -152,7 +152,7 @@
152152
"children": [
153153
{ "prover": "alt-ergo", "time": 0.033 },
154154
{ "prover": "alt-ergo", "time": 0.034 },
155-
{ "prover": "alt-ergo", "time": 0.048 },
155+
{ "prover": "z3", "time": 0.106 },
156156
{ "prover": "alt-ergo", "time": 0.036 }
157157
]
158158
},
@@ -161,7 +161,7 @@
161161
"children": [
162162
{ "prover": "alt-ergo", "time": 0.025 },
163163
{ "prover": "alt-ergo", "time": 0.027 },
164-
{ "prover": "alt-ergo", "time": 0.053 },
164+
{ "prover": "z3", "time": 0.163 },
165165
{ "prover": "alt-ergo", "time": 0.033 }
166166
]
167167
},
@@ -170,7 +170,7 @@
170170
"children": [
171171
{ "prover": "alt-ergo", "time": 0.027 },
172172
{ "prover": "alt-ergo", "time": 0.024 },
173-
{ "prover": "alt-ergo", "time": 0.043 },
173+
{ "prover": "alt-ergo", "time": 0.216 },
174174
{ "prover": "alt-ergo", "time": 0.033 }
175175
]
176176
},
@@ -179,7 +179,7 @@
179179
"children": [
180180
{ "prover": "alt-ergo", "time": 0.021 },
181181
{ "prover": "alt-ergo", "time": 0.025 },
182-
{ "prover": "alt-ergo", "time": 0.045 },
182+
{ "prover": "alt-ergo", "time": 0.217 },
183183
{ "prover": "alt-ergo", "time": 0.028 }
184184
]
185185
},
@@ -189,16 +189,16 @@
189189
"children": [
190190
{ "prover": "alt-ergo", "time": 0.031 },
191191
{ "prover": "alt-ergo", "time": 0.035 },
192-
{ "prover": "z3", "time": 0.106 },
193-
{ "prover": "alt-ergo", "time": 0.05 }
192+
{ "prover": "z3", "time": 0.267 },
193+
{ "prover": "alt-ergo", "time": 0.221 }
194194
]
195195
},
196196
{
197197
"tactic": "split_vc",
198198
"children": [
199199
{ "prover": "alt-ergo", "time": 0.039 },
200200
{ "prover": "alt-ergo", "time": 0.041 },
201-
{ "prover": "z3", "time": 0.083 },
201+
{ "prover": "z3", "time": 0.218 },
202202
{ "prover": "z3", "time": 0.051 }
203203
]
204204
},
@@ -214,18 +214,18 @@
214214
{
215215
"tactic": "split_vc",
216216
"children": [
217-
{ "prover": "alt-ergo", "time": 0.05 },
217+
{ "prover": "alt-ergo", "time": 0.247 },
218218
{ "prover": "alt-ergo", "time": 0.045 },
219219
{ "prover": "z3", "time": 0.209 },
220-
{ "prover": "alt-ergo", "time": 0.053 }
220+
{ "prover": "alt-ergo", "time": 0.214 }
221221
]
222222
},
223223
{
224224
"tactic": "split_vc",
225225
"children": [
226226
{ "prover": "alt-ergo", "time": 0.029 },
227-
{ "prover": "alt-ergo", "time": 0.064 },
228-
{ "prover": "z3", "time": 0.127 },
227+
{ "prover": "cvc4", "time": 0.14 },
228+
{ "prover": "z3", "time": 0.315 },
229229
{ "prover": "alt-ergo", "time": 0.04 }
230230
]
231231
},
@@ -234,8 +234,8 @@
234234
"children": [
235235
{ "prover": "alt-ergo", "time": 0.03 },
236236
{ "prover": "alt-ergo", "time": 0.031 },
237-
{ "prover": "z3", "time": 0.148 },
238-
{ "prover": "cvc5", "time": 0.105 }
237+
{ "prover": "z3", "time": 0.427 },
238+
{ "prover": "alt-ergo", "time": 0.914 }
239239
]
240240
},
241241
{ "prover": "z3", "time": 0.242 },
@@ -246,7 +246,7 @@
246246
{ "prover": "z3", "time": 0.079 },
247247
{ "prover": "z3", "time": 0.057 },
248248
{ "prover": "z3", "time": 0.087 },
249-
{ "prover": "cvc5", "time": 0.22 },
249+
{ "prover": "z3", "time": 0.173 },
250250
{
251251
"tactic": "split_vc",
252252
"children": [
@@ -292,7 +292,7 @@
292292
"tactic": "split_vc",
293293
"children": [
294294
{ "prover": "alt-ergo", "time": 0.031 },
295-
{ "prover": "z3", "time": 0.388 },
295+
{ "prover": "z3", "time": 0.43 },
296296
{ "prover": "alt-ergo", "time": 0.053 },
297297
{ "prover": "z3", "time": 0.02 },
298298
{ "prover": "alt-ergo", "time": 0.022 },
@@ -352,22 +352,22 @@
352352
"tactic": "split_vc",
353353
"children": [
354354
{ "prover": "z3", "time": 0.03 },
355-
{ "prover": "z3", "time": 0.126 },
355+
{ "prover": "z3", "time": 0.209 },
356356
{ "prover": "z3", "time": 0.075 },
357357
{ "prover": "z3", "time": 0.073 },
358358
{
359359
"tactic": "split_vc",
360360
"children": [
361361
{ "prover": "alt-ergo", "time": 0.051 },
362362
{ "prover": "alt-ergo", "time": 0.036 },
363-
{ "prover": "alt-ergo", "time": 0.097 }
363+
{ "prover": "alt-ergo", "time": 0.483 }
364364
]
365365
},
366366
{ "prover": "z3", "time": 0.191 },
367367
{
368368
"tactic": "split_vc",
369369
"children": [
370-
{ "prover": "alt-ergo", "time": 0.047 },
370+
{ "prover": "alt-ergo", "time": 0.211 },
371371
{ "prover": "alt-ergo", "time": 0.029 },
372372
{ "prover": "z3", "time": 0.036 }
373373
]
@@ -376,23 +376,23 @@
376376
"tactic": "split_vc",
377377
"children": [
378378
{ "prover": "alt-ergo", "time": 0.07 },
379-
{ "prover": "alt-ergo", "time": 0.056 },
379+
{ "prover": "alt-ergo", "time": 0.228 },
380380
{ "prover": "z3", "time": 0.073 }
381381
]
382382
},
383383
{ "prover": "z3", "time": 0.177 },
384-
{ "prover": "z3", "time": 0.198 },
384+
{ "prover": "z3", "time": 0.322 },
385385
{
386386
"tactic": "split_vc",
387387
"children": [
388388
{ "prover": "alt-ergo", "time": 0.029 },
389389
{ "prover": "alt-ergo", "time": 0.033 },
390-
{ "prover": "alt-ergo", "time": 0.053 }
390+
{ "prover": "z3", "time": 0.044 }
391391
]
392392
},
393-
{ "prover": "z3", "time": 0.259 },
393+
{ "prover": "z3", "time": 0.197 },
394394
{ "prover": "z3", "time": 0.107 },
395-
{ "prover": "z3", "time": 0.144 },
395+
{ "prover": "z3", "time": 0.211 },
396396
{ "prover": "z3", "time": 0.117 },
397397
{ "prover": "z3", "time": 0.052 },
398398
{ "prover": "z3", "time": 0.031 },
@@ -408,7 +408,7 @@
408408
{ "prover": "z3", "time": 0.052 },
409409
{ "prover": "z3", "time": 0.033 },
410410
{ "prover": "z3", "time": 0.101 },
411-
{ "prover": "z3", "time": 0.236 },
411+
{ "prover": "z3", "time": 0.12 },
412412
{ "prover": "z3", "time": 0.047 },
413413
{ "prover": "z3", "time": 0.177 }
414414
]

‎examples/doubly_linked_list/proof.json‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
"M_example": {
55
"vc_cursor_front_i32": { "prover": "alt-ergo", "time": 0.013 },
66
"vc_eq_Option_i32": { "prover": "alt-ergo", "time": 0.019 },
7-
"vc_example": { "prover": "alt-ergo", "time": 0.574 },
7+
"vc_example": { "prover": "alt-ergo", "time": 1.1 },
88
"vc_get_i32": { "prover": "alt-ergo", "time": 0.009 },
99
"vc_insert_after_i32": { "prover": "alt-ergo", "time": 0.021 },
1010
"vc_insert_before_i32": { "prover": "alt-ergo", "time": 0.019 },
@@ -108,7 +108,7 @@
108108
"prover": "alt-ergo",
109109
"time": 0.026
110110
},
111-
"vc_insert_after_T": { "prover": "z3", "time": 0.348 },
111+
"vc_insert_after_T": { "prover": "z3", "time": 0.762 },
112112
"vc_insert_ghost_Box_Perm_ptr_Node_T_Global": {
113113
"prover": "alt-ergo",
114114
"time": 0.025
@@ -147,7 +147,7 @@
147147
"prover": "alt-ergo",
148148
"time": 0.026
149149
},
150-
"vc_insert_before_T": { "prover": "z3", "time": 0.49 },
150+
"vc_insert_before_T": { "prover": "z3", "time": 1.5 },
151151
"vc_insert_ghost_Box_Perm_ptr_Node_T_Global": {
152152
"prover": "alt-ergo",
153153
"time": 0.023
@@ -399,10 +399,10 @@
399399
{ "prover": "alt-ergo", "time": 0.046 },
400400
{ "prover": "z3", "time": 0.02 },
401401
{ "prover": "alt-ergo", "time": 0.037 },
402-
{ "prover": "z3", "time": 0.87 },
402+
{ "prover": "z3", "time": 1.7 },
403403
{
404404
"tactic": "compute_specified",
405-
"children": [ { "prover": "z3", "time": 0.469 } ]
405+
"children": [ { "prover": "z3", "time": 1.7 } ]
406406
},
407407
{ "prover": "alt-ergo", "time": 0.036 },
408408
{ "prover": "alt-ergo", "time": 0.035 },

‎examples/gnome_sort/proof.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636
{ "prover": "alt-ergo", "time": 0.029 },
3737
{ "prover": "alt-ergo", "time": 0.025 },
3838
{ "prover": "alt-ergo", "time": 0.034 },
39-
{ "prover": "cvc5", "time": 0.123 },
39+
{ "prover": "alt-ergo", "time": 0.107 },
4040
{ "prover": "alt-ergo", "time": 0.041 },
4141
{ "prover": "alt-ergo", "time": 0.042 },
4242
{ "prover": "alt-ergo", "time": 0.031 }

‎examples/haystack/proof.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
"vc_new_usize": { "prover": "cvc5", "time": 0.013 },
1919
"vc_next_RangeInclusive_usize": { "prover": "cvc5", "time": 0.014 },
2020
"vc_next_Range_usize": { "prover": "cvc5", "time": 0.017 },
21-
"vc_search": { "prover": "z3", "time": 0.236 }
21+
"vc_search": { "prover": "z3", "time": 0.475 }
2222
}
2323
}
2424
}

0 commit comments

Comments
 (0)