changeset 265:f4a0d5bc585c

Chapters 0.b/c: omit the executions that which SC results are indistinguishable from the racy ones
author shade
date Fri, 20 May 2016 00:30:06 +0300
parents 2a45a3af4a7e
children 73e599b8d13c
files jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java
diffstat 2 files changed, 73 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Thu May 19 23:22:35 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Fri May 20 00:30:06 2016 +0300
@@ -184,22 +184,21 @@
                 scResults.add(results);
             }
 
-            // TODO: Figure out the set of all possible results
-            Set<Map<Result, Value>> allResults = null;
+            Set<Map<Result, Value>> allResults = mt.racyResults();
 
-            if (allResults != null) {
-                // regardless of the reorderings, all results appear SC.
-                //    => the violations are undetectable
-                if (!allResults.containsAll(scResults)) {
-                    System.out.println(scResults);
-                    System.out.println(allResults);
-                    throw new IllegalStateException("SC results should be subset of all results");
-                }
+            if (!allResults.containsAll(scResults)) {
+                System.out.println(mt.canonicalId());
+                System.out.println(scResults);
+                System.out.println(allResults);
+                throw new IllegalStateException("SC results should be subset of all results");
+            }
 
-                if (scResults.equals(allResults)) {
-                    // nothing to do here,
-                    continue;
-                }
+            // regardless of the reorderings, all results appear SC.
+            //    => the violations are undetectable
+
+            if (scResults.equals(allResults)) {
+                // nothing to do here,
+                continue;
             }
 
             List<String> mappedResult = new ArrayList<>();
@@ -656,6 +655,51 @@
             return threads.size() > 1;
         }
 
+        public Set<Result> allResults() {
+            return threads.stream()
+                    .flatMap(t -> t.ops.stream())
+                    .filter(op -> op.getType() == Op.Type.LOAD)
+                    .map(Op::getResult)
+                    .collect(Collectors.toSet());
+        }
+
+        public Set<Value> allValues() {
+            return threads.stream()
+                    .flatMap(t -> t.ops.stream())
+                    .filter(op -> op.getType() == Op.Type.STORE)
+                    .map(Op::getValue)
+                    .collect(Collectors.toSet());
+        }
+
+        /**
+         * @return The set of outcomes where every load can see every store.
+         */
+        public Set<Map<Result, Value>> racyResults() {
+            Set<Map<Result, Value>> allResults = new HashSet<>();
+            allResults.add(new HashMap<>());
+
+            for (Result r : allResults()) {
+                Set<Map<Result, Value>> temp = new HashSet<>();
+
+                for (Map<Result, Value> sub : allResults) {
+                    for (Value v : allValues()) {
+                        Map<Result, Value> newMap = new HashMap<>(sub);
+                        newMap.put(r, v);
+                        temp.add(newMap);
+                    }
+
+                    {
+                        Map<Result, Value> newMap = new HashMap<>(sub);
+                        newMap.put(r, Value.defaultOne());
+                        temp.add(newMap);
+                    }
+                }
+
+                allResults = temp;
+            }
+
+            return allResults;
+        }
     }
 
 }
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java	Thu May 19 23:22:35 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java	Fri May 20 00:30:06 2016 +0300
@@ -54,4 +54,19 @@
     public String toString() {
         return "" + v;
     }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+
+        Value value = (Value) o;
+
+        return v == value.v;
+    }
+
+    @Override
+    public int hashCode() {
+        return v;
+    }
 }