changeset 270:99df9f47b864

Generators: make sure SeqCstTraceGenerator generates the interesting test shapes.
author shade
date Mon, 23 May 2016 01:37:01 +0300
parents 220566d5a284
children fbc00f951b21
files jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/MultiThread.java jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Trace.java jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java
diffstat 4 files changed, 59 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/MultiThread.java	Sun May 22 01:12:29 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/MultiThread.java	Mon May 23 01:37:01 2016 +0300
@@ -123,6 +123,7 @@
             }
             sb.append("_");
         }
+        sb.delete(sb.length() - 2, sb.length());
         return sb.toString();
     }
 
@@ -133,17 +134,6 @@
         return true;
     }
 
-    public boolean hasNoThreadsWithSameLoads() {
-        Set<String> eq = new HashSet<>();
-        for (Trace trace : threads) {
-            if (trace.storeCount() == 0) {
-                if (!eq.add(trace.id()))
-                    return false;
-            }
-        }
-        return true;
-    }
-
     public boolean hasNoIntraThreadPairs() {
         Multiset<Integer> vars = new HashMultiset<>();
         for (Trace trace : threads) {
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Sun May 22 01:12:29 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Mon May 23 01:37:01 2016 +0300
@@ -31,6 +31,7 @@
 import java.io.FileNotFoundException;
 import java.io.PrintWriter;
 import java.util.*;
+import java.util.concurrent.ConcurrentHashMap;
 import java.util.stream.Collectors;
 
 public class SeqCstTraceGenerator {
@@ -149,28 +150,24 @@
         /*
            Step 4. Apply more filters to reduce
          */
+        Set<String> canonicalIds = Collections.newSetFromMap(new ConcurrentHashMap<>());
 
-        multiThreads = multiThreads.stream()
+        multiThreads = multiThreads.parallelStream()
                 .filter(MultiThread::isMultiThread)               // really have multiple threads
                 .filter(MultiThread::hasNoSingleLoadThreads)      // threads with single loads produce duplicate tests
-                .filter(MultiThread::hasNoThreadsWithSameLoads)   // threads with the same loads produce duplicate tests
                 .filter(MultiThread::hasNoIntraThreadPairs)       // has no operations that do not span threads
-                .collect(Collectors.toList());
-
-        System.out.print(multiThreads.size() + " interesting... ");
-
-        Set<String> canonicalIds = new HashSet<>();
-        multiThreads = multiThreads.stream()
                 .filter(mt -> canonicalIds.add(mt.canonicalId())) // pass only one canonical
                 .collect(Collectors.toList());
 
-        System.out.println(multiThreads.size() + " unique.");
+        System.out.println(multiThreads.size() + " interesting.");
 
         /*
             Step 5. Figure out what executions are sequentially consistent (needed for grading!),
             and emit the tests.
          */
 
+        Set<String> generatedIds = new HashSet<>();
+
         System.out.print("Figuring out SC outcomes for the testcases: ");
         int testCount = 0;
         for (MultiThread mt : multiThreads) {
@@ -191,14 +188,15 @@
                 throw new IllegalStateException("SC results should be subset of all results");
             }
 
-            // regardless of the reorderings, all results appear SC.
-            //    => the violations are undetectable
-
             if (scResults.equals(allResults)) {
+                // all racy results are indistinguishable from SC
+                //    => the violations are undetectable
                 // nothing to do here,
                 continue;
             }
 
+            generatedIds.add(mt.canonicalId());
+
             List<String> mappedResult = new ArrayList<>();
             for (Map<Result, Value> m : scResults) {
                 List<String> mappedValues = new ArrayList<>();
@@ -213,12 +211,52 @@
         }
         System.out.println();
         System.out.println("Found " + testCount + " interesting test cases");
+
+        /*
+            Step 6. Check that no important cases were filtered.
+
+            The nomenclature is derived from Maranget, Sarkar, Sewell,
+              "A Tutorial Introduction to the ARM and POWER Relaxed Memory Models"
+         */
+        check(generatedIds, "L1_L2__S2_S1", "MP");
+
+        // TODO: Have mismatched stores: need arbiter to judge the final result
+        // check(generatedIds, "L1_S2__S2_S1", "S");
+        // check(generatedIds, "S1_L2__S2_S1", "R");
+        // check(generatedIds, "S1_S2__S2_S1", "2+2W");
+        // check(generatedIds, "L1_S2__S1__S2_L1", "WRW+WR");
+        // check(generatedIds, "L1_S2__S1__S2_S1", "WRR+2W");
+
+        check(generatedIds, "S1_L2__S2_L1", "SB");
+        check(generatedIds, "L1_S2__L2_S1", "LB");
+
+        check(generatedIds, "L1_L2__L2_S1__S2", "WRC");
+        check(generatedIds, "L1_S2__L2_S1__S1", "WWC");
+        check(generatedIds, "L1_L2__S1__S2_L1", "RWC");
+        check(generatedIds, "L1_L2__S1__S2_S1", "WRR+2W");
+
+        check(generatedIds, "L1_L2__S2_S1", "PPO");
+        check(generatedIds, "L1_L2__L2_L1__S1__S2", "IRIW");
+        check(generatedIds, "L1_L2__L2_S1__S1__S2", "IRRWIW");
+        check(generatedIds, "L1_S2__L2_S1__S1__S2", "IRWIW");
+
+        check(generatedIds, "L1_L1__S1_S1", "CoRR0");
+        check(generatedIds, "L1_L1__S1", "CoRR1");
+        check(generatedIds, "L1_L1__L1_L1__S1__S1", "CoRR2");
+        check(generatedIds, "L1_S1__S1", "CoRW");
+        check(generatedIds, "S1__S1_L1", "CoWR");
+    }
+
+    private void check(Set<String> ids, String id, String info) {
+        if (!ids.contains(id)) {
+            throw new IllegalStateException("Generated cases should contain " + info);
+        }
     }
 
     private void emit(MultiThread mt, List<String> scResults) {
         String pathname = Utils.ensureDir(srcDir + "/" + pkg.replaceAll("\\.", "/"));
 
-        String klass = mt.canonicalId() + "Test";
+        String klass = mt.canonicalId() + "_Test";
 
         Class[] klasses = new Class[mt.loadCount()];
         for (int c = 0; c < klasses.length; c++) {
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Trace.java	Sun May 22 01:12:29 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Trace.java	Mon May 23 01:37:01 2016 +0300
@@ -214,7 +214,7 @@
     }
 
     public void assignResults() {
-        Value.reset();
+        int valId = Value.initial();
         int resId = 1;
         for (int c = 0; c < ops.size(); c++) {
             Op op = ops.get(c);
@@ -224,7 +224,7 @@
                     break;
                 }
                 case STORE: {
-                    ops.set(c, Op.newStore(op, Value.newOne()));
+                    ops.set(c, Op.newStore(op, Value.newOne(valId++)));
                     break;
                 }
                 default:
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java	Sun May 22 01:12:29 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Value.java	Mon May 23 01:37:01 2016 +0300
@@ -26,25 +26,19 @@
 
 public class Value {
 
-    private static int id;
-
-    {
-        reset();
+    static int initial() {
+        return 1;
     }
 
-    static void reset() {
-        id = 1;
-    }
-
-    static Value newOne() {
-        return new Value(id++);
+    static Value newOne(int id) {
+        return new Value(id);
     }
 
     static Value defaultOne() {
         return new Value(0);
     }
 
-    private int v;
+    private final int v;
 
     public Value(int v) {
         this.v = v;