Skip to content
Snippets Groups Projects
Commit 6047253d authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Thread safety concerns due to "memory barrier" pattern in value classes.

Logical backport of Github issue #439
https://github.com/tlaplus/tlaplus/issues/439

[Bug][TLC]
parent 50e52565
No related branches found
No related tags found
No related merge requests found
...@@ -7,7 +7,6 @@ ...@@ -7,7 +7,6 @@
package tlc2.value.impl; package tlc2.value.impl;
import java.io.IOException; import java.io.IOException;
import java.util.Arrays;
import java.util.Map; import java.util.Map;
import tlc2.tool.EvalControl; import tlc2.tool.EvalControl;
...@@ -30,7 +29,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -30,7 +29,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
public final IntervalValue intv; public final IntervalValue intv;
public final Value[] values; public final Value[] values;
private boolean isNorm; private boolean isNorm;
private int[] indexTbl; // speed up function application
public static final Value EmptyFcn = new FcnRcdValue(new Value[0], new Value[0], true); public static final Value EmptyFcn = new FcnRcdValue(new Value[0], new Value[0], true);
/* Constructor */ /* Constructor */
...@@ -39,7 +37,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -39,7 +37,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values; this.values = values;
this.intv = null; this.intv = null;
this.isNorm = isNorm; this.isNorm = isNorm;
this.indexTbl = null;
} }
public FcnRcdValue(IntervalValue intv, Value[] values) { public FcnRcdValue(IntervalValue intv, Value[] values) {
...@@ -47,7 +44,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -47,7 +44,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values; this.values = values;
this.domain = null; this.domain = null;
this.isNorm = true; this.isNorm = true;
this.indexTbl = null;
} }
public FcnRcdValue(IntervalValue intv, Value[] values, CostModel cm) { public FcnRcdValue(IntervalValue intv, Value[] values, CostModel cm) {
...@@ -60,7 +56,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -60,7 +56,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.intv = fcn.intv; this.intv = fcn.intv;
this.values = values; this.values = values;
this.isNorm = fcn.isNorm; this.isNorm = fcn.isNorm;
this.indexTbl = fcn.indexTbl;
} }
public FcnRcdValue(ValueVec elems, Value[] values, boolean isNorm) { public FcnRcdValue(ValueVec elems, Value[] values, boolean isNorm) {
...@@ -80,45 +75,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -80,45 +75,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
@Override @Override
public final byte getKind() { return FCNRCDVALUE; } public final byte getKind() { return FCNRCDVALUE; }
/* We create an index only when the domain is not very small. */
private final void createIndex() {
if (this.domain != null && this.domain.length > 10) {
int len = this.domain.length * 2 + 1;
int[] tbl = new int[len];
Arrays.fill(tbl, -1);
synchronized(this) {
for (int i = 0; i < this.domain.length; i++) {
int loc = (this.domain[i].hashCode() & 0x7FFFFFFF) % len;
while (tbl[loc] != -1) {
loc = (loc + 1) % len;
}
tbl[loc] = i;
}
}
synchronized(this) { this.indexTbl = tbl; }
}
}
private final int lookupIndex(Value arg) {
int len = this.indexTbl.length;
int loc = (arg.hashCode() & 0x7FFFFFFF) % len;
while (true) {
int idx = this.indexTbl[loc];
if (idx == -1) {
Assert.fail("Attempted to apply function:\n" + Values.ppr(this.toString()) +
"\nto argument " + Values.ppr(arg.toString()) +
", which is not in the domain of the function.");
}
if (this.domain[idx].equals(arg)) {
return idx;
}
loc = (loc + 1) % len;
}
}
@Override @Override
public final int compareTo(Object obj) { public final int compareTo(Object obj) {
try { try {
...@@ -348,15 +304,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -348,15 +304,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
} }
else { else {
// domain is represented as an array of values: // domain is represented as an array of values:
if (this.indexTbl != null) {
return this.values[this.lookupIndex(arg)];
}
if (this.isNorm) this.createIndex();
if (this.indexTbl != null) {
return this.values[this.lookupIndex(arg)];
}
else {
int len = this.domain.length; int len = this.domain.length;
for (int i = 0; i < len; i++) { for (int i = 0; i < len; i++) {
if (this.domain[i].equals(arg)) { if (this.domain[i].equals(arg)) {
...@@ -364,7 +311,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue { ...@@ -364,7 +311,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
} }
} }
} }
}
return null; return null;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment