Skip to content

Commit

Permalink
Enable passing a percentage as a value for --cores (#3357)
Browse files Browse the repository at this point in the history
Fixes #3328

```
  --cores <count>                         Run the Dafny CLI using <n> cores, or using 
                                          <XX%> of the machine's logical cores. 
                                          [default: 6]
```

Default is 50% of logical cores. Sadly the help shows that number
already being resolved. Changing that is complicated.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer authored Jan 17, 2023
1 parent a75e209 commit bcf4042
Showing 5 changed files with 68 additions and 7 deletions.
34 changes: 32 additions & 2 deletions Source/DafnyCore/Options/BoogieOptionBag.cs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
using System;
using System.Collections.Generic;
using System.CommandLine;
using System.Linq;
using System.Transactions;
using Microsoft.Boogie;

namespace Microsoft.Dafny;
@@ -17,8 +19,34 @@ public static class BoogieOptionBag {
ArgumentHelpName = "arguments",
};

public static readonly Option<uint> Cores = new("--cores", () => 0,
"Run the Dafny CLI using <n> cores. Specifying 0 will use half of the available processor cores.") {
public static readonly Option<uint> Cores = new("--cores", result => {
if (result.Tokens.Count != 1) {
result.ErrorMessage = $"Expected only one value for option {Cores.Name}";
return 1;
}

var value = result.Tokens[0].Value;
if (value.EndsWith('%')) {
if (double.TryParse(value.Substring(0, value.Length - 1), out var percentage)) {
return Math.Max(1U, (uint)(percentage / 100.0 * Environment.ProcessorCount));
}

result.ErrorMessage = $"Could not parse percentage {value}";
return 1;
}

if (uint.TryParse(value, out var number)) {
if (number > 0) {
return number;
}

result.ErrorMessage = $"Number of cores to use must be greater than 0";
return 1;
}
result.ErrorMessage = $"Could not parse number {value}";
return 1;
}, true,
"Run the Dafny verifier using <n> cores, or using <XX%> of the machine's logical cores.") {
ArgumentHelpName = "count"
};

@@ -33,6 +61,8 @@ public static class BoogieOptionBag {
};

static BoogieOptionBag() {
Cores.SetDefaultValue((uint)((Environment.ProcessorCount + 1) / 2));

DafnyOptions.RegisterLegacyBinding(BoogieFilter, (o, f) => o.ProcsToCheck.AddRange(f));
DafnyOptions.RegisterLegacyBinding(BoogieArguments, (o, boogieOptions) => {

10 changes: 8 additions & 2 deletions Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs
Original file line number Diff line number Diff line change
@@ -38,6 +38,12 @@ public static LitCommandWithRedirection Parse(string[] tokens, LitTestConfigurat
errorFile = config.ApplySubstitutions(argumentsList[redirectErrorIndex + 1]).Single();
argumentsList.RemoveRange(redirectErrorIndex, 2);
}
var redirectErrorAppendIndex = argumentsList.IndexOf("2>>");
if (redirectErrorAppendIndex >= 0) {
errorFile = config.ApplySubstitutions(argumentsList[redirectErrorAppendIndex + 1]).Single();
appendOutput = true;
argumentsList.RemoveRange(redirectErrorAppendIndex, 2);
}

var arguments = argumentsList.SelectMany(config.ApplySubstitutions);

@@ -69,7 +75,7 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string?
public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inReader, TextWriter? outWriter, TextWriter? errWriter) {
var inputReader = inputFile != null ? new StreamReader(inputFile) : null;
var outputWriter = outputFile != null ? new StreamWriter(outputFile, append) : null;
var errorWriter = errorFile != null ? new StreamWriter(errorFile, false) : null;
var errorWriter = errorFile != null ? new StreamWriter(errorFile, append) : null;
var result = command.Execute(outputHelper, inputReader, outputWriter, errorWriter);
inputReader?.Close();
outputWriter?.Close();
@@ -95,4 +101,4 @@ public override string ToString() {
return builder.ToString();
}
}
}
}
8 changes: 7 additions & 1 deletion Test/cli/zeroCores.dfy
Original file line number Diff line number Diff line change
@@ -1,4 +1,10 @@
// RUN: ! %baredafny verify --use-basename-for-filename --cores=0 "%s" > "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=0 "%s" 2> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga "%s" 2>> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga% "%s" 2>> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename "%s" >> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=1 "%s" >> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=0% "%s" >> "%t"
// RUN: ! %baredafny verify --use-basename-for-filename --cores=50% "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"

method Foo() ensures false {
22 changes: 20 additions & 2 deletions Test/cli/zeroCores.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,4 +1,22 @@
zeroCores.dfy(4,27): Error: A postcondition might not hold on this return path.
zeroCores.dfy(4,21): Related location: This is the postcondition that might not hold.
Number of cores to use must be greater than 0

Could not parse number earga

Could not parse percentage earga%

zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error
zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error
zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error
zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.

Dafny program verifier finished with 0 verified, 1 error
1 change: 1 addition & 0 deletions docs/dev/news/3328.feat
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Enable passing a percentage value to the --cores option, to use a percentage of the total number of logical cores on the machine for verification.

0 comments on commit bcf4042

Please sign in to comment.