diff --git a/Comparison.md b/Comparison.md
index f1c2dc1..5afdf3f 100644
--- a/Comparison.md
+++ b/Comparison.md
@@ -87,7 +87,7 @@ Size is also a better representation of comparison especially for collections or
There are examples where increasing on one axis while decreasing on others can lead to smaller cases e.g. if Version fails for `2 * ma + mi + bu ≥ 255 * 2`
CsCheck will be able to shrink to `255.0.0` but [Hedgehog](https://github.com/hedgehogqa) won't.
-For concurrency testing random shrinkers also has an advantage. Concurrency tests may not fail deterministically.
+For parallel testing random shrinkers also has an advantage. Parallel tests may not fail deterministically.
This is a real problem for path explorer shrinkers. The only solution is to repeat each test multiple times (10 for QuickCheck) since they need to follow defined paths.
For a random shrinker you can just continue testing different random cases until one fails and limit the size to that each time.
diff --git a/CsCheck/Check.cs b/CsCheck/Check.cs
index 5c9df9d..8a6d184 100644
--- a/CsCheck/Check.cs
+++ b/CsCheck/Check.cs
@@ -25,7 +25,7 @@ public static partial class Check
public static long Iter = ParseEnvironmentVariableToLong("CsCheck_Iter", 100);
/// The number of seconds to run the sample.
public static int Time = ParseEnvironmentVariableToInt("CsCheck_Time" , -1);
- /// The number of times to retry the seed to reproduce a SampleConcurrent fail (default 100).
+ /// The number of times to retry the seed to reproduce a SampleParallel fail (default 100).
public static int Replay = ParseEnvironmentVariableToInt("CsCheck_Replay", 100);
/// The number of threads to run the sample on (default number logical CPUs).
public static int Threads = ParseEnvironmentVariableToInt("CsCheck_Threads", Environment.ProcessorCount);
@@ -1277,9 +1277,9 @@ public static Task SampleAsync(this Gen<(T1, T2,
Action? writeLine = null, string? seed = null, long iter = -1, int time = -1, int threads = -1, Func<(T1, T2, T3, T4, T5, T6, T7, T8), string>? print = null)
=> SampleAsync(gen, t => predicate(t.Item1, t.Item2, t.Item3, t.Item4, t.Item5, t.Item6, t.Item7, t.Item8), writeLine, seed, iter, time, threads, print);
- sealed class ModelBasedData(Actual actualState, Model modelState, uint stream, ulong seed, (string, Action)[] operations)
+ sealed class ModelBasedData(Actual actualState, Model modelState, uint stream, ulong seed, (string, Action, Action)[] operations)
{
- public Actual ActualState = actualState; public Model ModelState = modelState; public uint Stream = stream; public ulong Seed = seed; public (string, Action)[] Operations = operations; public Exception? Exception;
+ public Actual ActualState = actualState; public Model ModelState = modelState; public uint Stream = stream; public ulong Seed = seed; public (string, Action, Action)[] Operations = operations; public Exception? Exception;
}
sealed class GenInitial(Gen<(Actual, Model)> initial) : Gen<(Actual Actual, Model Model, uint Stream, ulong Seed)>
@@ -1316,12 +1316,12 @@ public static void SampleModelBased(this Gen<(Actual, Model)> ini
printActual ??= Print;
printModel ??= Print;
- var opNameActions = new Gen<(string, Action)>[operations.Length];
+ var opNameActions = new Gen<(string, Action, Action)>[operations.Length];
for (int i = 0; i < operations.Length; i++)
{
var op = operations[i];
var opName = "Op" + i;
- opNameActions[i] = op.AddOpNumber ? op.Select(t => (opName + t.Item1, t.Item2)) : op;
+ opNameActions[i] = op.AddOpNumber ? op.Select(t => (opName + t.Item1, t.Item2, t.Item3)) : op;
}
new GenInitial(initial)
@@ -1331,7 +1331,10 @@ public static void SampleModelBased(this Gen<(Actual, Model)> ini
try
{
foreach (var operation in d.Operations)
- operation.Item2(d.ActualState, d.ModelState);
+ {
+ operation.Item2(d.ActualState);
+ operation.Item3(d.ModelState);
+ }
return equal(d.ActualState, d.ModelState);
}
catch (Exception e)
@@ -1567,14 +1570,32 @@ public static void SampleMetamorphic(this Gen initial, GenMetamorphic o
});
}
- sealed class ConcurrentData(T state, uint stream, ulong seed, (string, Action)[] operations, int threads)
+ sealed class SampleParallelData(T state, uint stream, ulong seed, (string, Action)[] sequencialOperations, (string, Action)[] parallelOperations, int threads)
{
- public T State = state; public uint Stream = stream; public ulong Seed = seed; public (string, Action)[] Operations = operations; public int Threads = threads; public int[]? ThreadIds; public Exception? Exception;
+ public T InitialState = state;
+ public uint Stream = stream;
+ public ulong Seed = seed;
+ public (string, Action)[] SequencialOperations = sequencialOperations;
+ public (string, Action)[] ParallelOperations = parallelOperations;
+ public int Threads = threads;
+ public int[]? ThreadIds;
+ public Exception? Exception;
}
- internal const int MAX_CONCURRENT_OPERATIONS = 10;
+ sealed class SampleParallelData(Actual actual, Model model, uint stream, ulong seed, (string, Action, Action)[] sequencialOperations, (string, Action, Action)[] parallelOperations, int threads)
+ {
+ public Actual InitialActual = actual;
+ public Model InitialModel = model;
+ public uint Stream = stream;
+ public ulong Seed = seed;
+ public (string, Action, Action)[] SequencialOperations = sequencialOperations;
+ public (string, Action, Action)[] ParallelOperations = parallelOperations;
+ public int Threads = threads;
+ public int[]? ThreadIds;
+ public Exception? Exception;
+ }
- sealed class GenConcurrent(Gen initial) : Gen<(T Value, uint Stream, ulong Seed)>
+ sealed class GenSampleParallel(Gen initial) : Gen<(T Value, uint Stream, ulong Seed)>
{
public override (T, uint, ulong) Generate(PCG pcg, Size? min, out Size size)
{
@@ -1584,22 +1605,35 @@ public override (T, uint, ulong) Generate(PCG pcg, Size? min, out Size size)
}
}
- /// Sample model-based operations on a random initial state concurrently.
+ sealed class GenSampleParallel(Gen<(Actual, Model)> initial) : Gen<(Actual Actual, Model Model, uint Stream, ulong Seed)>
+ {
+ public override (Actual, Model, uint, ulong) Generate(PCG pcg, Size? min, out Size size)
+ {
+ var stream = pcg.Stream;
+ var seed = pcg.Seed;
+ var (actual, model) = initial.Generate(pcg, null, out size);
+ return (actual, model, stream, seed);
+ }
+ }
+
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// The operation generators that can act on the state concurrently.
+ /// The operation generators that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
/// A function to convert the state to a string for error reporting (default Check.Print).
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
- public static void SampleConcurrent(this Gen initial, GenOperation[] operations, Func? equal = null, string? seed = null,
- long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ public static void SampleParallel(this Gen initial, GenOperation[] operations, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
{
equal ??= Equal;
seed ??= Seed;
@@ -1626,12 +1660,14 @@ public static void SampleConcurrent(this Gen initial, GenOperation[] op
bool firstIteration = true;
- new GenConcurrent(initial)
- .Select(Gen.OneOf(opNameActions).Array[1, MAX_CONCURRENT_OPERATIONS]
- .SelectMany(ops => Gen.Int[1, Math.Min(threads, ops.Length)].Select(i => (ops, i))), (a, b) =>
- new ConcurrentData(a.Value, a.Stream, a.Seed, b.ops, b.i)
- )
- .Sample(cd =>
+ var genOps = Gen.OneOf(opNameActions);
+ Gen.Int[2, maxParallelOperations]
+ .SelectMany(np => Gen.Int[2, Math.Min(threads, np)].Select(nt => (nt, np)))
+ .SelectMany((nt, np) => Gen.Int[0, maxSequentialOperations].Select(ns => (ns, nt, np)))
+ .SelectMany((ns, nt, np) => new GenSampleParallel(initial).Select(genOps.Array[ns], genOps.Array[np])
+ .Select((initial, sequencial, parallel) => (initial, sequencial, nt, parallel)))
+ .Select((initial, sequencial, threads, parallel) => new SampleParallelData(initial.Value, initial.Stream, initial.Seed, sequencial, parallel, threads))
+ .Sample(spd =>
{
bool linearizable = false;
do
@@ -1639,22 +1675,22 @@ public static void SampleConcurrent(this Gen initial, GenOperation[] op
try
{
if (replayThreads is null)
- Run(cd.State, cd.Operations, cd.Threads, cd.ThreadIds = new int[cd.Operations.Length]);
+ Run(spd.InitialState, spd.SequencialOperations, spd.ParallelOperations, spd.Threads, spd.ThreadIds = new int[spd.ParallelOperations.Length]);
else
- RunReplay(cd.State, cd.Operations, cd.Threads, cd.ThreadIds = replayThreads);
+ RunReplay(spd.InitialState, spd.SequencialOperations, spd.ParallelOperations, spd.Threads, spd.ThreadIds = replayThreads);
}
catch (Exception e)
{
- cd.Exception = e;
+ spd.Exception = e;
break;
}
- Parallel.ForEach(Permutations(cd.ThreadIds, cd.Operations), (sequence, state) =>
+ Parallel.ForEach(Permutations(spd.ThreadIds, spd.ParallelOperations), (sequence, state) =>
{
- var linearState = initial.Generate(new PCG(cd.Stream, cd.Seed), null, out _);
+ var linearState = initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _);
try
{
- Run(linearState, sequence, 1);
- if (equal(cd.State, linearState))
+ Run(linearState, spd.SequencialOperations, sequence, 1);
+ if (equal(spd.InitialState, linearState))
{
linearizable = true;
state.Stop();
@@ -1666,30 +1702,31 @@ public static void SampleConcurrent(this Gen initial, GenOperation[] op
firstIteration = false;
return linearizable;
}, writeLine, seed, iter, time, threads: 1,
- p =>
+ spd =>
{
print ??= Print;
- if (p == null) return "";
+ if (spd == null) return "";
var sb = new StringBuilder();
- sb.Append("\n Operations: ").Append(Print(p.Operations.Select(i => i.Item1).ToList()));
- sb.Append("\n On Threads: ").Append(Print(p.ThreadIds));
- sb.Append("\nInitial state: ").Append(print(initial.Generate(new PCG(p.Stream, p.Seed), null, out _)));
- sb.Append("\n Final state: ").Append(p.Exception is not null ? p.Exception.ToString() : print(p.State));
+ sb.Append("\n Initial state: ").Append(print(initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _)));
+ sb.Append("\nSequencial Operations: ").Append(Print(spd.SequencialOperations.Select(i => i.Item1).ToList()));
+ sb.Append("\n Parallel Operations: ").Append(Print(spd.ParallelOperations.Select(i => i.Item1).ToList()));
+ sb.Append("\n On Threads: ").Append(Print(spd.ThreadIds));
+ sb.Append("\n Final state: ").Append(spd.Exception is not null ? spd.Exception.ToString() : print(spd.InitialState));
bool first = true;
- foreach (var sequence in Permutations(p.ThreadIds!, p.Operations))
+ foreach (var sequence in Permutations(spd.ThreadIds!, spd.ParallelOperations))
{
- var linearState = initial.Generate(new PCG(p.Stream, p.Seed), null, out _);
+ var linearState = initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _);
string result;
try
{
- Run(linearState, sequence, 1);
+ Run(linearState, spd.SequencialOperations, sequence, 1);
result = print(linearState);
}
catch (Exception e)
{
result = e.ToString();
}
- sb.Append(first ? "\n Linearized: " : "\n : ");
+ sb.Append(first ? "\n Linearized: " : "\n : ");
sb.Append(Print(sequence.Select(i => i.Item1).ToList()));
sb.Append(" -> ");
sb.Append(result);
@@ -1699,14 +1736,16 @@ public static void SampleConcurrent(this Gen initial, GenOperation[] op
});
}
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1714,19 +1753,21 @@ public static void SampleConcurrent(this Gen initial, GenOperation[] op
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation, Func? equal = null, string? seed = null,
- long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
- => SampleConcurrent(initial, [operation], equal, seed, iter, time, threads, print, replay, writeLine);
+ public static void SampleParallel(this Gen initial, GenOperation operation, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1734,20 +1775,22 @@ public static void SampleConcurrent(this Gen initial, GenOperation oper
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation1, GenOperation operation2, Func? equal = null,
- string? seed = null, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
- => SampleConcurrent(initial, [operation1, operation2], equal, seed, iter, time, threads, print, replay, writeLine);
+ public static void SampleParallel(this Gen initial, GenOperation operation1, GenOperation operation2, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1755,21 +1798,23 @@ public static void SampleConcurrent(this Gen initial, GenOperation oper
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, Func? equal = null,
- string? seed = null, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
- => SampleConcurrent(initial, [operation1, operation2, operation3], equal, seed, iter, time, threads, print, replay, writeLine);
+ public static void SampleParallel(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1777,23 +1822,24 @@ public static void SampleConcurrent(this Gen initial, GenOperation oper
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4,
- Func? equal = null, string? seed = null, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1,
- Action? writeLine = null)
- => SampleConcurrent(initial, [operation1, operation2, operation3, operation4], equal, seed, iter, time, threads, print, replay, writeLine);
+ public static void SampleParallel(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3, operation4], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1801,25 +1847,26 @@ public static void SampleConcurrent(this Gen initial, GenOperation oper
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4,
- GenOperation operation5, Func? equal = null, string? seed = null, long iter = -1, int time = -1, int threads = -1, Func? print = null,
+ public static void SampleParallel(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, GenOperation operation5, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null,
int replay = -1, Action? writeLine = null)
- => SampleConcurrent(initial, [operation1, operation2, operation3, operation4, operation5],
- equal, seed, iter, time, threads, print, replay, writeLine);
+ => SampleParallel(initial, [operation1, operation2, operation3, operation4, operation5], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
- /// Sample model-based operations on a random initial state concurrently.
+ /// Sample operations on a random initial state in parallel.
/// The result is compared against the result of the possible sequential permutations.
- /// At least one of these permutations result must be equal for the concurrency to have been linearized successfully.
+ /// At least one of these permutations result must be equal for the parallel execution to have been linearized successfully.
/// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
/// The initial state generator.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
- /// An operation generator that can act on the state concurrently.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
+ /// An operation generator that can act on the state in parallel.
/// A function to check if the two states are the same (default Check.Equal).
/// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
/// The number of iterations to run in the sample (default 100).
/// The number of seconds to run the sample.
/// The number of threads to run the sample on (default number logical CPUs).
@@ -1827,11 +1874,277 @@ public static void SampleConcurrent(this Gen initial, GenOperation oper
/// The number of times to retry the seed to reproduce an initial fail (default 100).
/// WriteLine function to use for the summary total iterations output.
[MethodImpl(MethodImplOptions.AggressiveInlining)]
- public static void SampleConcurrent(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4,
- GenOperation operation5, GenOperation operation6, Func? equal = null, string? seed = null, long iter = -1, int time = -1, int threads = -1,
- Func? print = null, int replay = -1, Action? writeLine = null)
- => SampleConcurrent(initial, [operation1, operation2, operation3, operation4, operation5, operation6],
- equal, seed, iter, time, threads, print, replay, writeLine);
+ public static void SampleParallel(this Gen initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, GenOperation operation5, GenOperation operation6, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? print = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3, operation4, operation5, operation6], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, print, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// The actual and model operation generators that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation[] operations, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ {
+ equal ??= ModelEqual;
+ seed ??= Seed;
+ if (iter == -1) iter = Iter;
+ if (time == -1) time = Time;
+ if (threads == -1) threads = Threads;
+ if (replay == -1) replay = Replay;
+ int[]? replayThreads = null;
+ printActual ??= Print;
+ printModel ??= Print;
+ if (seed?.Contains('[') == true)
+ {
+ int i = seed.IndexOf('[');
+ int j = seed.IndexOf(']', i + 1);
+ replayThreads = seed.Substring(i + 1, j - i - 1).Split(',').Select(int.Parse).ToArray();
+ seed = seed[..i];
+ }
+
+ var opNameActions = new Gen<(string, Action, Action)>[operations.Length];
+ for (int i = 0; i < operations.Length; i++)
+ {
+ var op = operations[i];
+ var opName = "Op" + i;
+ opNameActions[i] = op.AddOpNumber ? op.Select((name, actual, model) => (opName + name, actual, model)) : op;
+ }
+
+ bool firstIteration = true;
+
+ var genOps = Gen.OneOf(opNameActions);
+ Gen.Int[2, maxParallelOperations]
+ .SelectMany(np => Gen.Int[2, Math.Min(threads, np)].Select(nt => (nt, np)))
+ .SelectMany((nt, np) => Gen.Int[0, maxSequentialOperations].Select(ns => (ns, nt, np)))
+ .SelectMany((ns, nt, np) => new GenSampleParallel(initial).Select(genOps.Array[ns], genOps.Array[np])
+ .Select((initial, sequencial, parallel) => (initial, sequencial, nt, parallel)))
+ .Select((initial, sequencial, threads, parallel) => new SampleParallelData(initial.Actual, initial.Model, initial.Stream, initial.Seed, sequencial, parallel, threads))
+ .Sample(spd =>
+ {
+ bool linearizable = false;
+ do
+ {
+ var actualSequencialOperations = Array.ConvertAll(spd.SequencialOperations, i => (i.Item1, i.Item2));
+ var actualParallelOperations = Array.ConvertAll(spd.ParallelOperations, i => (i.Item1, i.Item2));
+ try
+ {
+ if (replayThreads is null)
+ Run(spd.InitialActual, actualSequencialOperations, actualParallelOperations, spd.Threads, spd.ThreadIds = new int[spd.ParallelOperations.Length]);
+ else
+ RunReplay(spd.InitialActual, actualSequencialOperations, actualParallelOperations, spd.Threads, spd.ThreadIds = replayThreads);
+ }
+ catch (Exception e)
+ {
+ spd.Exception = e;
+ break;
+ }
+ var modelSequencialOperations = Array.ConvertAll(spd.SequencialOperations, i => (i.Item1, i.Item3));
+ var modelParallelOperations = Array.ConvertAll(spd.ParallelOperations, i => (i.Item1, i.Item3));
+ Parallel.ForEach(Permutations(spd.ThreadIds, modelParallelOperations), (sequence, state) =>
+ {
+ var (_, initialModel) = initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _);
+ try
+ {
+ Run(initialModel, modelSequencialOperations, sequence, 1);
+ if (equal(spd.InitialActual, initialModel))
+ {
+ linearizable = true;
+ state.Stop();
+ }
+ }
+ catch { state.Stop(); }
+ });
+ } while (linearizable && firstIteration && seed is not null && --replay > 0);
+ firstIteration = false;
+ return linearizable;
+ }, writeLine, seed, iter, time, threads: 1,
+ spd =>
+ {
+ if (spd == null) return "";
+ var sb = new StringBuilder();
+ sb.Append("\n Initial state: ").Append(printActual(initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _).Item1));
+ sb.Append("\nSequencial Operations: ").Append(Print(spd.SequencialOperations.Select(i => i.Item1).ToList()));
+ sb.Append("\n Parallel Operations: ").Append(Print(spd.ParallelOperations.Select(i => i.Item1).ToList()));
+ sb.Append("\n On Threads: ").Append(Print(spd.ThreadIds));
+ sb.Append("\n Final state: ").Append(spd.Exception is not null ? spd.Exception.ToString() : printActual(spd.InitialActual));
+ var modelSequencialOperations = Array.ConvertAll(spd.SequencialOperations, i => (i.Item1, i.Item3));
+ var modelParallelOperations = Array.ConvertAll(spd.ParallelOperations, i => (i.Item1, i.Item3));
+ bool first = true;
+ foreach (var sequence in Permutations(spd.ThreadIds!, modelParallelOperations))
+ {
+ var (_, initialModel) = initial.Generate(new PCG(spd.Stream, spd.Seed), null, out _);
+ string result;
+ try
+ {
+ Run(initialModel, modelSequencialOperations, sequence, 1);
+ result = printModel(initialModel);
+ }
+ catch (Exception e)
+ {
+ result = e.ToString();
+ }
+ sb.Append(first ? "\n Linearized: " : "\n : ");
+ sb.Append(Print(sequence.Select(i => i.Item1).ToList()));
+ sb.Append(" -> ");
+ sb.Append(result);
+ first = false;
+ }
+ return sb.ToString();
+ });
+ }
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, printActual, printModel, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation1, GenOperation operation2, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, printActual, printModel, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, printActual, printModel, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3, operation4], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, printActual, printModel, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, GenOperation operation5, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func? printActual = null, Func? printModel = null, int replay = -1, Action? writeLine = null)
+ => SampleParallel(initial, [operation1, operation2, operation3, operation4, operation5], equal, seed, maxSequentialOperations, maxParallelOperations, iter, time, threads, printActual, printModel, replay, writeLine);
+
+ /// Sample operations on the random initial actual state in parallel and compare to all the possible linearized operations run sequencially on the initial model state.
+ /// At least one of these permutations model result must be equal for the parallel execution to have been linearized successfully.
+ /// If not the failing initial state and sequence will be shrunk down to the shortest and simplest.
+ /// The initial actual and model state generator.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// An actual and model operation generator that can act on the state in parallel. There is no need for the model operations to be thread safe as they are only run sequencially.
+ /// A function to check if the actual and model are the same (default Check.ModelEqual).
+ /// The initial seed to use for the first iteration.
+ /// The maximum number of operations to run sequentially before the parallel operations (default of 10).
+ /// The maximum number of operations to run in parallel (default of 5).
+ /// The number of iterations to run in the sample (default 100).
+ /// The number of seconds to run the sample.
+ /// The number of threads to run the sample on (default number logical CPUs).
+ /// A function to convert the actual state to a string for error reporting (default Check.Print).
+ /// A function to convert the model state to a string for error reporting (default Check.Print).
+ /// The number of times to retry the seed to reproduce an initial fail (default 100).
+ /// WriteLine function to use for the summary total iterations output.
+ [MethodImpl(MethodImplOptions.AggressiveInlining)]
+ public static void SampleParallel(this Gen<(Actual, Model)> initial, GenOperation operation1, GenOperation operation2, GenOperation operation3, GenOperation operation4, GenOperation operation5, GenOperation operation6, Func? equal = null, string? seed = null,
+ int maxSequentialOperations = 10, int maxParallelOperations = 5, long iter = -1, int time = -1, int threads = -1, Func