Fix a slightly non-deterministic behavior in the Monoids benchmark

When built with output enabled, sometimes a few lines would be
interchanged, depending on the order in which parallel tasks
complete. Simplify the dispatcher logic a bit to ensure we get
the same output ordering every time.

This does not impact the running time of the benchmark.
This commit is contained in:
Slava Pestov
2025-09-19 12:03:50 -04:00
parent 3e981b7d8f
commit 575c7097f6

View File

@@ -1,6 +1,8 @@
/// This file implements the driver loop which attempts Knuth-Bendix completion /// This file implements the driver loop which attempts Knuth-Bendix completion
/// with various strategies on all instances in parallel. /// with various strategies on all instances in parallel.
let numTasks = 32
struct Dispatcher { struct Dispatcher {
let subset: [Int] let subset: [Int]
let strategies: [Strategy] let strategies: [Strategy]
@@ -48,7 +50,7 @@ struct Solver {
mutating func solve() async { mutating func solve() async {
if output { if output {
print("# Remaining \(subset.count)") print("# Remaining \(subset.count)")
print("# n:\tpresentation:\tcardinality:\tcomplete presentation:\tstrategy:") print("# n:\tpresentation:\tcardinality:\tcomplete:\tstrategy:")
} }
// The shortlex order with identity permutation of generators solves // The shortlex order with identity permutation of generators solves
@@ -173,9 +175,8 @@ struct Solver {
mutating func attempt(_ strategies: [Strategy]) async { mutating func attempt(_ strategies: [Strategy]) async {
if subset.isEmpty { return } if subset.isEmpty { return }
let solved = await withTaskGroup(of: (Int, Int, Solution?).self) { group in await withTaskGroup(of: (Int, Int, Solution?).self) { group in
var dispatcher = Dispatcher(subset: subset, var dispatcher = Dispatcher(subset: subset, strategies: strategies)
strategies: strategies)
var solved: [Int: (Int, Solution)] = [:] var solved: [Int: (Int, Solution)] = [:]
var pending: [Int: Int] = [:] var pending: [Int: Int] = [:]
@@ -216,6 +217,7 @@ struct Solver {
// The lowest-numbered strategy is the 'official' solution for the instance. // The lowest-numbered strategy is the 'official' solution for the instance.
var betterStrategy = true var betterStrategy = true
if let (oldStrategyIndex, _) = solved[instance] { if let (oldStrategyIndex, _) = solved[instance] {
precondition(oldStrategyIndex != strategyIndex)
if oldStrategyIndex < strategyIndex { if oldStrategyIndex < strategyIndex {
betterStrategy = false betterStrategy = false
} }
@@ -226,56 +228,57 @@ struct Solver {
} }
} }
retireStrategies() while retireStrategy() {}
} }
func retireStrategies() { func retireStrategy() -> Bool {
var retired: [Int: [Int]] = [:] // Check if nothing remains.
let pendingInOrder = pending.sorted { $0.key < $1.key } guard let minPending = pending.keys.min() else { return false }
for (strategyIndex, numTasks) in pendingInOrder {
precondition(strategyIndex <= dispatcher.currentStrategy)
if dispatcher.currentStrategy == strategyIndex { break }
if numTasks > 0 { break }
pending[strategyIndex] = nil // Check if we're going to dispatch more instances with this strategy.
retired[strategyIndex] = [] precondition(minPending <= dispatcher.currentStrategy)
} if minPending == dispatcher.currentStrategy { return false }
if retired.isEmpty { return } // Check if we're still waiting for instances to finish with this
// strategy.
if pending[minPending]! > 0 { return false }
// If we are done dispatching a strategy, look at all instances solved // Otherwise, retire this strategy.
// by that strategy and print them out. pending[minPending] = nil
for n in subset {
if let (strategyIndex, solution) = solved[n] {
if retired[strategyIndex] != nil {
retired[strategyIndex]!.append(n)
// Print the instance and solution. // Print out all instances solved by this strategy and remove them
var str = "\(n + 1)\t\(instances[n])\t" // from the list.
subset = subset.filter { n in
guard let (strategyIndex, solution) = solved[n] else { return true }
guard strategyIndex == minPending else { return true }
if let cardinality = solution.cardinality { // Print the instance and solution.
str += "finite:\(cardinality)" var str = "\(n + 1)\t\(instances[n])\t"
finite[cardinality, default: 0] += 1
} else {
str += "infinite"
}
str += "\tfcrs:\(solution.presentation)"
// Print the extra generators that were added, if any. if let cardinality = solution.cardinality {
if !solution.extra.isEmpty { str += "finite:\(cardinality)"
str += "\t\(printRules(solution.extra))" finite[cardinality, default: 0] += 1
} } else {
str += "infinite"
if output {
print(str)
}
}
} }
str += "\tfcrs:\(solution.presentation)"
// Print the extra generators that were added, if any.
if !solution.extra.isEmpty {
str += "\t\(printRules(solution.extra))"
}
if output {
print(str)
}
return false
} }
return true
} }
// We run 32 tasks at a time. for _ in 0 ..< numTasks {
for _ in 0 ..< 32 {
startTask() startTask()
} }
@@ -283,10 +286,6 @@ struct Solver {
startTask() startTask()
completeTask(instance, strategyIndex, solution) completeTask(instance, strategyIndex, solution)
} }
return solved
} }
subset = subset.filter { solved[$0] == nil }
} }
} }