Per John's suggestion. Litmus (and rmem, and, should it ever be a c4t backend, phenolphthalein) all track the number of times a particular state was observed. This would be useful for testing as it would help us characterise which bugs appear to be concurrency related (eg, only appear in some of the occurrences).
Really, the Obs struct needs refactoring anyway: something along the lines of
type Obs struct {
Flags Flag
States []State
}
type State struct {
Kind StateKind
Occs int
Vars map[string]string
}
type StateKind uint8
const (
KindUnknown StateKind = iota
KindWitness
KindCounterExample
)
with various predicates for getting witness and counter-example []State.
Per John's suggestion. Litmus (and rmem, and, should it ever be a c4t backend, phenolphthalein) all track the number of times a particular state was observed. This would be useful for testing as it would help us characterise which bugs appear to be concurrency related (eg, only appear in some of the occurrences).
Really, the
Obsstruct needs refactoring anyway: something along the lines ofwith various predicates for getting witness and counter-example []State.