This is an automated email from the ASF dual-hosted git repository.
dcapwell pushed a commit to branch trunk
in repository https://gitbox.apache.org/repos/asf/cassandra-accord.git
The following commit(s) were added to refs/heads/trunk by this push:
new 5626c7c CASSANDRA-17112: Publish StrictSerializabilityVerifier so
Cassandra may use, and fixed bugs found with the integration (#18)
5626c7c is described below
commit 5626c7c11400d4cf6d01a8e22517b53a83f5c512
Author: dcapwell <[email protected]>
AuthorDate: Mon Jan 23 11:45:13 2023 -0800
CASSANDRA-17112: Publish StrictSerializabilityVerifier so Cassandra may
use, and fixed bugs found with the integration (#18)
---
accord-core/build.gradle | 9 +
.../main/java/accord/impl/SimpleProgressLog.java | 9 +-
.../test/java/accord/verify/HistoryViolation.java | 4 +
.../verify/StrictSerializabilityVerifier.java | 153 ++++++++++-----
.../verify/StrictSerializabilityVerifierTest.java | 216 ++++++++++++++++++++-
5 files changed, 330 insertions(+), 61 deletions(-)
diff --git a/accord-core/build.gradle b/accord-core/build.gradle
index 7db65e9..146f9fa 100644
--- a/accord-core/build.gradle
+++ b/accord-core/build.gradle
@@ -48,6 +48,10 @@ task burn(type: JavaExec) {
// the team is used to 'install' so make sure that still publishes locally
task install(dependsOn: publishToMavenLocal)
+task testJar(type: Jar, dependsOn: testClasses) {
+ archiveClassifier = 'tests'
+ from sourceSets.test.output
+}
publishing {
publications {
@@ -58,6 +62,11 @@ publishing {
}
from components.java
}
+
+ test(MavenPublication) {
+ artifactId = 'accord'
+ artifact testJar
+ }
}
}
diff --git a/accord-core/src/main/java/accord/impl/SimpleProgressLog.java
b/accord-core/src/main/java/accord/impl/SimpleProgressLog.java
index 7fff500..e27553f 100644
--- a/accord-core/src/main/java/accord/impl/SimpleProgressLog.java
+++ b/accord-core/src/main/java/accord/impl/SimpleProgressLog.java
@@ -126,11 +126,12 @@ public class SimpleProgressLog implements
ProgressLog.Factory
{
switch (progress)
{
- default: throw new AssertionError();
+ default: throw new AssertionError("Unexpected
progress: " + progress);
case NoneExpected:
case Done:
+ return false;
case Investigating:
- throw new IllegalStateException();
+ throw new IllegalStateException("Unexpected
progress: " + progress);
case Expected:
Invariants.paranoid(!isFree());
progress = NoProgress;
@@ -209,11 +210,11 @@ public class SimpleProgressLog implements
ProgressLog.Factory
setProgress(Investigating);
switch (status)
{
- default: throw new AssertionError();
+ default: throw new AssertionError("Unexpected status:
" + status);
case NotWitnessed: // can't make progress if we
haven't witnessed it yet
case Committed: // can't make progress if we aren't
yet ReadyToExecute
case Done: // shouldn't be trying to make progress, as
we're done
- throw new IllegalStateException();
+ throw new IllegalStateException("Unexpected
status: " + status);
case Uncommitted:
case ReadyToExecute:
diff --git a/accord-core/src/test/java/accord/verify/HistoryViolation.java
b/accord-core/src/test/java/accord/verify/HistoryViolation.java
index 5df0573..6e31ceb 100644
--- a/accord-core/src/test/java/accord/verify/HistoryViolation.java
+++ b/accord-core/src/test/java/accord/verify/HistoryViolation.java
@@ -27,4 +27,8 @@ public class HistoryViolation extends AssertionError
super(detailMessage);
this.primaryKey = primaryKey;
}
+
+ public int primaryKey() {
+ return primaryKey;
+ }
}
diff --git
a/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifier.java
b/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifier.java
index 44374c1..98e6217 100644
--- a/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifier.java
+++ b/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifier.java
@@ -30,7 +30,9 @@ import java.util.TreeSet;
import java.util.function.Consumer;
import java.util.stream.IntStream;
-import accord.utils.Invariants;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+import static java.util.stream.Collectors.joining;
/**
* Nomenclature:
@@ -43,34 +45,36 @@ import accord.utils.Invariants;
* two kinds: 1) those values for keys [B,C..) at step index i
for a read of key A, precede key A's step index i +1
* 2) those values for keys [B,C..) at step index i
for a write of key A, precede key A's step index i
* max predecessor: the maximum predecessor that may be reached via any
predecessor relation
- *
+ * <p>
* Ensure there are no timestamp cycles in the implied list of predecessors,
i.e. that we have a strict serializable order.
* That is, we maintain links to the maximum predecessor step for each key, at
each step for each key, and see if we can
* find a path of predecessors that would witness us.
- *
+ * <p>
* TODO (low priority): find and report a path when we encounter a violation
*/
public class StrictSerializabilityVerifier
{
+ private static final Logger logger =
LoggerFactory.getLogger(StrictSerializabilityVerifier.class);
+
/**
* A link to the maximum predecessor node for a given key reachable from
the transitive closure of predecessor
* relations from a given register's observation (i.e. for a given
sequence observed for a given key).
- *
+ * <p>
* A predecessor is an absolute happens-before relationship. This is
created either:
* 1) by witnessing some read for key A coincident with a write for key B,
* therefore the write for key B happened strictly after the write for
key A; or
* 2) any value for key A witnessed alongside a step index i for key B
happens before i+1 for key B.
- *
+ * <p>
* For every observation step index i for key A, we have an outgoing
MaxPredecessor link to every key.
* This object both maintains the current maximum predecessor step index
reachable via the transitive closure
* of happens-before relationships, but represents a back-link from that
step index for the referred-to key,
* so that when its own predecessor memoized maximum predecessor values
are updated we can propagate them here.
- *
+ * <p>
* In essence, each node in the happens-before graph maintains a link to
every possible frontier of its transitive
* closure in the graph, so that each time that frontier is updated the
internal nodes that reference it are updated
* to the new frontier. This ensures ~computationally optimal maintenance
of this transitive closure at the expense
* of quadratic memory utilisation, but for small numbers of unique keys
this remains quite manageable (i.e. steps*keys^2)
- *
+ * <p>
* This graph can be interpreted quite simply: if any step index for a key
can reach itself (or a successor) via
* the transitive closure of happens-before relations then there is a
serializability violation.
*/
@@ -143,6 +147,7 @@ public class StrictSerializabilityVerifier
static class UnknownStepPredecessor extends MaxPredecessor
{
final UnknownStepHolder holder;
+
UnknownStepPredecessor(Step successor, UnknownStepHolder holder)
{
super(successor.ofKey, successor, holder.step.ofKey);
@@ -228,6 +233,7 @@ public class StrictSerializabilityVerifier
Map<Step, UnknownStepPredecessor> unknownStepPredecessors;
Runnable onChange;
+ final int writeValue;
int ofStepIndex;
/**
@@ -247,9 +253,10 @@ public class StrictSerializabilityVerifier
int maxPredecessorWrittenAfter = Integer.MIN_VALUE;
- Step(int key, int stepIndex, int keyCount)
+ Step(int key, int stepIndex, int keyCount, int writeValue)
{
super(key, null, key);
+ this.writeValue = writeValue;
this.ofStep = this;
this.ofStepIndex = stepIndex;
this.maxPeers = new int[keyCount];
@@ -312,21 +319,21 @@ public class StrictSerializabilityVerifier
successor.predecessorStep = this;
}
- boolean updatePeers(int[] newPeers, UnknownStepHolder[] unknownSteps)
+ boolean updatePeers(int[] newPeerSteps, UnknownStepHolder[]
newBlindWrites)
{
boolean updated = false;
- for (int key = 0 ; key < newPeers.length ; ++key)
+ for (int key = 0 ; key < newPeerSteps.length ; ++key)
{
- int newPeer = newPeers[key];
+ int newPeer = newPeerSteps[key];
int maxPeer = maxPeers[key];
if (newPeer > maxPeer)
{
updated = true;
- maxPeers[key] = newPeers[key];
+ maxPeers[key] = newPeerSteps[key];
}
- if (unknownSteps != null)
+ if (newBlindWrites != null)
{
- UnknownStepHolder unknownStep = unknownSteps[key];
+ UnknownStepHolder unknownStep = newBlindWrites[key];
if (unknownStep != null && unknownStep.step != this)
{
if (unknownStepPeers == null)
@@ -443,23 +450,29 @@ public class StrictSerializabilityVerifier
@Override
public String toString()
{
- return "{key: " + ofKey +
- ", peers:" + Arrays.toString(maxPeers) +
- ", preds:" + Arrays.toString(maxPredecessors) +
- (unknownStepPeers != null ? ", peers?:" + unknownStepPeers
: "") +
- (unknownStepPredecessors != null ? ", preds?:" +
unknownStepPredecessors.values() : "") +
- "}";
+ StringBuilder builder = new StringBuilder("{key: " + ofKey);
+ if (ofStepIndex < 0)
+ builder.append(", value: ").append(writeValue);
+ builder.append(", peers:").append(Arrays.toString(maxPeers))
+ .append(",
preds:").append(Arrays.toString(maxPredecessors))
+ .append(unknownStepPeers != null ? ", peers?:" +
unknownStepPeers : "")
+ .append(unknownStepPredecessors != null ? ", preds?:" +
unknownStepPredecessors.values() : "")
+ .append("}");
+ return builder.toString();
}
}
+ // TODO (expected, testing): rethink this concept - should it be a Step?
Does it provide any value? If not, it's more confusing.
class FutureWrites extends Step
{
-
/**
* Any write value we don't know the step index for because we did not
perform a coincident read;
* we wait until we witness a read containing the
- *
- * TODO (desired, testing): handle writes with unknown outcome
+ * <p>
+ * TODO: report a violation if we have witnessed a sequence missing
any of these deferred operations
+ * that started after they finished
+ * <p>
+ * TODO: handle writes with unknown outcome
*/
final Map<Integer, UnknownStepHolder> byWriteValue = new HashMap<>();
@@ -467,7 +480,7 @@ public class StrictSerializabilityVerifier
FutureWrites(int key, int keyCount)
{
- super(key, Integer.MAX_VALUE, keyCount);
+ super(key, Integer.MAX_VALUE, keyCount, Integer.MIN_VALUE);
}
void newSequence(int[] oldSequence, int[] newSequence)
@@ -489,10 +502,16 @@ public class StrictSerializabilityVerifier
recompute();
}
+ @Override
+ boolean witnessedBetween(int start, int end, boolean isWrite)
+ {
+ return false;
+ }
+
@Override
boolean updatePeers(int[] newPeers, UnknownStepHolder[] unknownSteps)
{
- return unknownSteps[ofKey].step.updatePeers(newPeers,
unknownSteps);
+ return false;
}
@Override
@@ -506,9 +525,14 @@ public class StrictSerializabilityVerifier
@Override
boolean updatePredecessorsOfWrite(int[][] reads, int[] writes,
StrictSerializabilityVerifier verifier)
{
- for (UnknownStepHolder holder : byWriteValue.values())
- holder.step.updatePredecessorsOfWrite(reads, writes, verifier);
- return super.updatePredecessorsOfWrite(reads, writes, verifier);
+ // TODO (required): this evidently wasn't carefully considered at
the time, and removing it improves things
+ // but what if anything this trying to achieve?
+ // probably we DO want to update the predecessors
of any NEW step. perhaps we also want
+ // and we probably want some additional unit
tests around blind writes
+// for (UnknownStepHolder holder : byWriteValue.values())
+// holder.step.updatePredecessorsOfWrite(reads, writes,
verifier);
+// return super.updatePredecessorsOfWrite(reads, writes, verifier);
+ return false;
}
void recompute()
@@ -520,15 +544,15 @@ public class StrictSerializabilityVerifier
witnessedBetween(deferred.start, deferred.end, true);
}
- void register(UnknownStepHolder[] unknownSteps, int start, int end)
+ void register(UnknownStepHolder[] newBlindWrites, int start, int end)
{
- UnknownStepHolder unknownStep = unknownSteps[ofKey];
+ UnknownStepHolder unknownStep = newBlindWrites[ofKey];
if (null != byWriteValue.putIfAbsent(unknownStep.writeValue,
unknownStep))
throw new AssertionError();
if (null != byTimestamp.putIfAbsent(end, unknownStep))
throw new AssertionError();
// TODO (desired, testing): verify this propagation by unit test
- unknownSteps[ofKey].step.receiveKnowledgePhasedPredecessors(this,
StrictSerializabilityVerifier.this);
+
newBlindWrites[ofKey].step.receiveKnowledgePhasedPredecessors(this,
StrictSerializabilityVerifier.this);
}
public void checkForUnwitnessed(int start)
@@ -539,6 +563,11 @@ public class StrictSerializabilityVerifier
throw new HistoryViolation(ofKey, "Writes not witnessed: " +
notWitnessed);
}
}
+
+ public String toString()
+ {
+ return "FutureWrites:[" + byTimestamp.values().stream().map(s ->
s.writeValue).map(Object::toString).collect(joining(",")) + ']';
+ }
}
/**
@@ -559,6 +588,12 @@ public class StrictSerializabilityVerifier
this.futureWrites = new FutureWrites(key, keyCount);
}
+ void print()
+ {
+ for (Map.Entry<Integer, UnknownStepHolder> e :
futureWrites.byWriteValue.entrySet())
+ logger.error("{}: {} -> ({}, {}, {})", key, e.getKey(),
e.getValue().writeValue, e.getValue().start, e.getValue().end);
+ }
+
private void updateSequence(int[] sequence, int maybeWrite)
{
for (int i = 0, max = Math.min(sequence.length,
this.sequence.length) ; i < max ; ++i)
@@ -592,7 +627,7 @@ public class StrictSerializabilityVerifier
steps = Arrays.copyOf(steps, Math.max(step + 1, steps.length *
2));
if (steps[step] == null)
- insert(new Step(key, step, keyCount));
+ insert(new Step(key, step, keyCount, step == 0 ? -1 :
sequence[step - 1]));
return steps[step];
}
@@ -618,28 +653,27 @@ public class StrictSerializabilityVerifier
step.setSuccessor(successor);
propagateToDirectSuccessor(step, successor);
}
-
}
- private void updatePeersAndPredecessors(int[] newPeers, int[][] reads,
int[] writes, int start, int end, UnknownStepHolder[] unknownSteps)
+ private void updatePeersAndPredecessors(int[] newPeerSteps, int[][]
reads, int[] writes, int start, int end, UnknownStepHolder[] newBlindWrites)
{
Step step;
- boolean updated = false;
- if (newPeers[key] >= 0)
+ boolean updated;
+ if (newPeerSteps[key] >= 0)
{
- step = step(newPeers[key]);
+ step = step(newPeerSteps[key]);
}
- else if (unknownSteps != null && unknownSteps[key] != null)
+ else if (newBlindWrites != null && newBlindWrites[key] != null)
{
assert writes[key] >= 0;
- futureWrites.register(unknownSteps, start, end);
- step = futureWrites;
+ futureWrites.register(newBlindWrites, start, end);
+ step = newBlindWrites[key].step;
}
else
{
throw new IllegalStateException();
}
- updated = step.updatePeers(newPeers, unknownSteps);
+ updated = step.updatePeers(newPeerSteps, newBlindWrites);
updated |= step.updatePredecessorsOfWrite(reads, writes,
StrictSerializabilityVerifier.this);
updated |= step.witnessedBetween(start, end, writes[key] >= 0);
if (updated)
@@ -680,7 +714,13 @@ public class StrictSerializabilityVerifier
if (step.successor != null)
propagateToDirectSuccessor(step, step.successor);
if (step.onChange != null)
- step.onChange.run();
+ {
+ // prevent reentrancy
+ Runnable run = step.onChange;
+ step.onChange = null;
+ run.run();
+ step.onChange = run;
+ }
}
void checkForUnwitnessed(int start)
@@ -735,7 +775,7 @@ public class StrictSerializabilityVerifier
/**
* Buffer a new read observation.
- *
+ * <p>
* Note that this should EXCLUDE any witnessed write for this key.
* This is to simplify the creation of direct happens-before edges with
observations for other keys
* that are implied by the witnessing of a write (and is also marginally
more efficient).
@@ -774,21 +814,24 @@ public class StrictSerializabilityVerifier
{
int i = Arrays.binarySearch(registers[k].sequence,
bufWrites[k]);
if (i >= 0) bufNewPeerSteps[k] = i + 1;
- else bufUnknownSteps[k] = new UnknownStepHolder(bufWrites[k],
start, end, new Step(k, Integer.MAX_VALUE, keyCount));
+ else bufUnknownSteps[k] = new UnknownStepHolder(bufWrites[k],
start, end, new Step(k, Integer.MAX_VALUE, keyCount, bufWrites[k]));
hasUnknownSteps |= i < 0;
}
}
+ for (int k = 0; k < bufReads.length ; ++k)
+ {
+ if (bufReads[k] != null)
+ registers[k].updateSequence(bufReads[k], bufWrites[k]);
+ }
for (int k = 0; k < bufReads.length ; ++k)
{
if (bufWrites[k] >= 0 || bufReads[k] != null)
{
- if (bufReads[k] != null)
- registers[k].updateSequence(bufReads[k], bufWrites[k]);
-
registers[k].updatePeersAndPredecessors(bufNewPeerSteps,
bufReads, bufWrites, start, end, hasUnknownSteps ? bufUnknownSteps : null);
+ if (bufReads[k] != null)
+ registers[k].checkForUnwitnessed(start);
}
- registers[k].checkForUnwitnessed(start);
}
refreshTransitive();
@@ -801,4 +844,18 @@ public class StrictSerializabilityVerifier
registers[next.ofKey].propagateToSuccessor(next.predecessorStep,
next.ofStep);
}
}
+
+ public void print()
+ {
+ for (Register r : registers)
+ {
+ if (r == null) continue;
+ r.print();
+ }
+ }
+
+ public void print(int k)
+ {
+ registers[k].print();
+ }
}
diff --git
a/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifierTest.java
b/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifierTest.java
index 78eadf4..c78513f 100644
---
a/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifierTest.java
+++
b/accord-core/src/test/java/accord/verify/StrictSerializabilityVerifierTest.java
@@ -19,9 +19,15 @@
package accord.verify;
import java.util.ArrayList;
+import java.util.Arrays;
import java.util.List;
import java.util.function.Consumer;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import java.util.stream.Stream;
+import com.carrotsearch.hppc.IntHashSet;
+import com.carrotsearch.hppc.IntSet;
import org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.assertThrows;
@@ -43,14 +49,35 @@ public class StrictSerializabilityVerifierTest
History w(int writeKey, int writeSeq)
{
- return rw(writeKey, writeSeq, null);
+ return rw(writeKey, writeSeq, (int[])null);
+ }
+
+ History ws(int ... writes)
+ {
+ return rw(writes, (int[])null);
}
History rw(int writeKey, int writeSeq, int ... reads)
+ {
+ int[] writes;
+ if (writeKey < 0)
+ {
+ writes = new int[0];
+ }
+ else
+ {
+ writes = new int[writeKey + 1];
+ Arrays.fill(writes, -1);
+ writes[writeKey] = writeSeq;
+ }
+ return rw(writes, reads);
+ }
+
+ History rw(int[] writes, int ... reads)
{
int start = overlap > 0 ? this.overlap : ++nextAt;
int end = ++nextAt;
- observations.add(new Observation(writeKey, writeSeq, reads, start,
end));
+ observations.add(new Observation(writes, reads, start, end));
return this;
}
@@ -96,8 +123,11 @@ public class StrictSerializabilityVerifierTest
verifier.witnessRead(key,
SEQUENCES[observation.reads[key] + 1]);
}
}
- if (observation.writeKey >= 0)
- verifier.witnessWrite(observation.writeKey,
observation.writeSeq);
+ for (int j = 0 ; j < observation.writes.length ; ++j)
+ {
+ if (observation.writes[j] >= 0)
+ verifier.witnessWrite(j, observation.writes[j]);
+ }
if (i == observations.size() - 1) onLast.accept(() ->
verifier.apply(observation.start, observation.end));
else verifier.apply(observation.start, observation.end);
@@ -107,15 +137,13 @@ public class StrictSerializabilityVerifierTest
static class Observation
{
- final int writeKey;
- final int writeSeq;
+ final int[] writes;
final int[] reads;
final int start, end;
- Observation(int writeKey, int writeSeq, int[] reads, int start, int
end)
+ Observation(int[] writes, int[] reads, int start, int end)
{
- this.writeKey = writeKey;
- this.writeSeq = writeSeq;
+ this.writes = writes;
this.reads = reads;
this.start = start;
this.end = end;
@@ -167,4 +195,174 @@ public class StrictSerializabilityVerifierTest
new History(1).r(0).w(0, 1).r(1).assertNoViolation();
new History(1).rw(0, 1, 0).r(1).assertNoViolation();
}
+
+ @Test
+ public void blindWrites()
+ {
+ new History(2).ws(1, 1).r(1, -1).ws(-1, 2).assertNoViolation();
+ new History(2).ws(1, 1).ws(-1, 2).assertNoViolation();
+ new History(2).ws(1, 1).ws(2, 2).r(2).assertNoViolation();
+ new History(2).ws(1, 1).ws(2, 2).r(2).r(1).assertViolation();
+ new History(2).ws(1, 1).overlap().ws(2,
2).r(2).r(1).deoverlap().r(2).assertNoViolation();
+ new History(2).ws(1, 1).ws(2, 2).r(1).assertViolation();
+ }
+
+ private void fromLog(String log)
+ {
+ IntSet pks = new IntHashSet();
+ class Read
+ {
+ final int pk, id, count;
+ final int[] seq;
+
+ Read(int pk, int id, int count, int[] seq)
+ {
+ this.pk = pk;
+ this.id = id;
+ this.count = count;
+ this.seq = seq;
+ }
+ }
+ class Write
+ {
+ final int pk, id;
+ final boolean success;
+
+ Write(int pk, int id, boolean success)
+ {
+ this.pk = pk;
+ this.id = id;
+ this.success = success;
+ }
+ }
+ class Witness
+ {
+ final int start, end;
+ final List<Object> actions = new ArrayList<>();
+
+ Witness(int start, int end)
+ {
+ this.start = start;
+ this.end = end;
+ }
+
+ public void read(int pk, int id, int count, int[] seq)
+ {
+ actions.add(new Read(pk, id, count, seq));
+ }
+
+ public void write(int pk, int id, boolean success)
+ {
+ actions.add(new Write(pk, id, success));
+ }
+
+ public void process(StrictSerializabilityVerifier verifier)
+ {
+ verifier.begin();
+ for (Object a : actions)
+ {
+ if (a instanceof Read)
+ {
+ Read read = (Read) a;
+ verifier.witnessRead(read.pk, read.seq);
+ }
+ else
+ {
+ Write write = (Write) a;
+ if (write.success)
+ verifier.witnessWrite(write.pk, write.id);
+ }
+ }
+ verifier.apply(start, end);
+ }
+ }
+ List<Witness> witnesses = new ArrayList<>();
+ Witness current = null;
+ for (String line : log.split("\n"))
+ {
+ if (line.startsWith("Witness"))
+ {
+ if (current != null)
+ {
+ witnesses.add(current);
+ current = null;
+ }
+ Matcher matcher = Pattern.compile("Witness\\(start=(.+),
end=(.+)\\)").matcher(line);
+ if (!matcher.find()) throw new AssertionError("Unable to match
start/end of " + line);
+ current = new Witness(Integer.parseInt(matcher.group(1)),
Integer.parseInt(matcher.group(2)));
+ }
+ else if (line.startsWith("\tread"))
+ {
+ Matcher matcher = Pattern.compile("\tread\\(pk=(.+), id=(.+),
count=(.+), seq=\\[(.*)\\]\\)").matcher(line);
+ if (!matcher.find()) throw new AssertionError("Unable to match
read of " + line);
+ int pk = Integer.parseInt(matcher.group(1));
+ pks.add(pk);
+ int id = Integer.parseInt(matcher.group(2));
+ int count = Integer.parseInt(matcher.group(3));
+ String seqStr = matcher.group(4);
+ int[] seq = seqStr.isEmpty() ? new int[0] :
Stream.of(seqStr.split(",")).map(String::trim).mapToInt(Integer::parseInt).toArray();
+ current.read(pk, id, count, seq);
+ }
+ else if (line.startsWith("\twrite"))
+ {
+ Matcher matcher = Pattern.compile("\twrite\\(pk=(.+), id=(.+),
success=(.+)\\)").matcher(line);
+ if (!matcher.find()) throw new AssertionError("Unable to match
write of " + line);
+ int pk = Integer.parseInt(matcher.group(1));
+ pks.add(pk);
+ int id = Integer.parseInt(matcher.group(2));
+ boolean success = Boolean.parseBoolean(matcher.group(3));
+ current.write(pk, id, success);
+ }
+ else
+ {
+ throw new IllegalArgumentException("Unknow line: " + line);
+ }
+ }
+ if (current != null)
+ {
+ witnesses.add(current);
+ current = null;
+ }
+ int[] keys = pks.toArray();
+ Arrays.sort(keys);
+ StrictSerializabilityVerifier validator = new
StrictSerializabilityVerifier(3);
+ for (Witness w : witnesses)
+ {
+ w.process(validator);
+ }
+ }
+
+ @Test
+ public void seenBehavior()
+ {
+ fromLog("Witness(start=4, end=7)\n" +
+ "\tread(pk=0, id=2, count=0, seq=[])\n" +
+ "\twrite(pk=0, id=2, success=true)\n" +
+ "Witness(start=3, end=8)\n" +
+ "\tread(pk=2, id=0, count=0, seq=[])\n" +
+ "\twrite(pk=2, id=0, success=true)\n" +
+ "\twrite(pk=1, id=0, success=true)\n" +
+ "Witness(start=5, end=9)\n" +
+ "\tread(pk=0, id=3, count=1, seq=[2])\n" +
+ "\twrite(pk=0, id=3, success=true)\n" +
+ "Witness(start=2, end=10)\n" +
+ "\twrite(pk=2, id=1, success=true)\n" +
+ "\twrite(pk=1, id=1, success=true)\n" +
+ "Witness(start=6, end=11)\n" +
+ "\tread(pk=0, id=4, count=2, seq=[2, 3])\n" +
+ "\twrite(pk=0, id=4, success=true)\n" +
+ "Witness(start=12, end=14)\n" +
+ "\twrite(pk=0, id=5, success=true)\n" +
+ "Witness(start=13, end=16)\n" +
+ "\tread(pk=1, id=6, count=2, seq=[0, 1])\n" +
+ "\twrite(pk=1, id=6, success=true)\n" +
+ "\twrite(pk=2, id=6, success=true)\n" +
+ "Witness(start=15, end=18)\n" +
+ "\tread(pk=0, id=7, count=4, seq=[2, 3, 4, 5])\n" +
+ "\twrite(pk=0, id=7, success=true)\n" +
+ "Witness(start=17, end=20)\n" +
+ "\tread(pk=1, id=8, count=3, seq=[0, 1, 6])\n" +
+ "\twrite(pk=1, id=8, success=true)\n" +
+ "\twrite(pk=2, id=8, success=true)\n");
+ }
}
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
