From 6047253ddf40351b4c579296c0eceff7b83c7524 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Tue, 1 Feb 2022 21:25:00 -0800
Subject: [PATCH] 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]
---
.../src/tlc2/value/impl/FcnRcdValue.java | 54 -------------------
1 file changed, 54 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
index b8c18ab21..95e8619d9 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
@@ -7,7 +7,6 @@
package tlc2.value.impl;
import java.io.IOException;
-import java.util.Arrays;
import java.util.Map;
import tlc2.tool.EvalControl;
@@ -30,7 +29,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
public final IntervalValue intv;
public final Value[] values;
private boolean isNorm;
- private int[] indexTbl; // speed up function application
public static final Value EmptyFcn = new FcnRcdValue(new Value[0], new Value[0], true);
/* Constructor */
@@ -39,7 +37,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values;
this.intv = null;
this.isNorm = isNorm;
- this.indexTbl = null;
}
public FcnRcdValue(IntervalValue intv, Value[] values) {
@@ -47,7 +44,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values;
this.domain = null;
this.isNorm = true;
- this.indexTbl = null;
}
public FcnRcdValue(IntervalValue intv, Value[] values, CostModel cm) {
@@ -60,7 +56,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.intv = fcn.intv;
this.values = values;
this.isNorm = fcn.isNorm;
- this.indexTbl = fcn.indexTbl;
}
public FcnRcdValue(ValueVec elems, Value[] values, boolean isNorm) {
@@ -80,45 +75,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
@Override
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
public final int compareTo(Object obj) {
try {
@@ -348,22 +304,12 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
}
else {
// 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;
for (int i = 0; i < len; i++) {
if (this.domain[i].equals(arg)) {
return this.values[i];
}
}
- }
}
return null;
--
GitLab