changeset 272:ff8922143fdf

Generators: SeqCstTraceGenerator should check the final variable values too, unblocking the rest of interesting cases.
author shade
date Mon, 23 May 2016 17:12:38 +0300
parents fbc00f951b21
children 9b6b671dd1e0
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/TraceResult.java
diffstat 4 files changed, 185 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/MultiThread.java	Mon May 23 14:03:36 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/MultiThread.java	Mon May 23 17:12:38 2016 +0300
@@ -24,7 +24,9 @@
  */
 package org.openjdk.jcstress.generator.seqcst;
 
+import org.openjdk.jcstress.util.HashMultimap;
 import org.openjdk.jcstress.util.HashMultiset;
+import org.openjdk.jcstress.util.Multimap;
 import org.openjdk.jcstress.util.Multiset;
 
 import java.util.*;
@@ -170,10 +172,21 @@
                 .collect(Collectors.toSet());
     }
 
+    public Set<Integer> allVariables() {
+        return threads.stream()
+                .flatMap(t -> t.ops().stream())
+                .map(Op::getVarId)
+                .collect(Collectors.toSet());
+    }
+
     /**
      * @return The set of outcomes where every load can see every store.
      */
-    public Set<Map<Result, Value>> racyResults() {
+    public Set<TraceResult> racyResults() {
+        /*
+           Step 1. Produce all possible results:
+           (Results can see all writes
+         */
         Set<Map<Result, Value>> allResults = new HashSet<>();
         allResults.add(new HashMap<>());
 
@@ -197,7 +210,46 @@
             allResults = temp;
         }
 
-        return allResults;
+        /*
+           Step 2. Produce all possible variable values:
+         */
+        Multimap<Integer, Value> possibleValues = new HashMultimap<>();
+        for (Trace t : threads) {
+            for (Op op : t.ops()) {
+                if (op.isStore()) {
+                    possibleValues.put(op.getVarId(), op.getValue());
+                }
+            }
+        }
+
+        Set<Map<Integer, Value>> allValues = new HashSet<>();
+        allValues.add(new HashMap<>());
+
+        for (Integer varId : possibleValues.keys()) {
+            Set<Map<Integer, Value>> temp = new HashSet<>();
+
+            for (Map<Integer, Value> m : allValues) {
+                for (Value val : possibleValues.get(varId)) {
+                    Map<Integer, Value> newMap = new HashMap<>(m);
+                    newMap.put(varId, val);
+                    temp.add(newMap);
+                }
+            }
+
+            allValues = temp;
+        }
+
+        /*
+           Step 3. Results, product of all possible results and values:
+         */
+        Set<TraceResult> answer = new HashSet<>();
+        for (Map<Result, Value> results : allResults) {
+            for (Map<Integer, Value> values : allValues) {
+                answer.add(new TraceResult(results, values));
+            }
+        }
+
+        return answer;
     }
 
     public int loadCount() {
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Mon May 23 14:03:36 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/SeqCstTraceGenerator.java	Mon May 23 17:12:38 2016 +0300
@@ -98,9 +98,8 @@
 
         Set<String> canonicalTraces = new HashSet<>();
         traces = allTraces.stream()
-                .filter(Trace::hasLoads)            // Has observable effects
-                .filter(Trace::hasStores)           // Has modifications to observe
-                .filter(Trace::matchedLoadStores)   // All modifications are observed; no observing non-modified
+                .filter(Trace::hasStores)                          // Has modifications to observe
+                .filter(Trace::matchedLoads)                       // All loads have at least one matching store
                 .filter(t -> canonicalTraces.add(t.canonicalId())) // Only a canonical order of vars accepted
                 .collect(Collectors.toList());
 
@@ -171,15 +170,15 @@
         System.out.print("Figuring out SC outcomes for the testcases: ");
         int testCount = 0;
         for (MultiThread mt : multiThreads) {
-            Set<Map<Result, Value>> scResults = new HashSet<>();
+            Set<TraceResult> scResults = new HashSet<>();
 
             // Compute all SC results from the linearization of MT
             for (Trace linear : mt.linearize()) {
-                SortedMap<Result, Value> results = linear.interpret();
+                TraceResult results = linear.interpret();
                 scResults.add(results);
             }
 
-            Set<Map<Result, Value>> allResults = mt.racyResults();
+            Set<TraceResult> allResults = mt.racyResults();
 
             if (!allResults.containsAll(scResults)) {
                 System.out.println(mt.canonicalId());
@@ -197,15 +196,7 @@
 
             generatedIds.add(mt.canonicalId());
 
-            List<String> mappedResult = new ArrayList<>();
-            for (Map<Result, Value> m : scResults) {
-                List<String> mappedValues = new ArrayList<>();
-                for (Value v : m.values()) {
-                    mappedValues.add(v.toString());
-                }
-                mappedResult.add(mappedValues.toString());
-            }
-            emit(mt, mappedResult);
+            emit(mt, scResults);
             if ((testCount++ % 100) == 0)
                 System.out.print(".");
         }
@@ -220,19 +211,11 @@
          */
         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, "L1_S2__S2_L3__S3_S1", "Z6.0");
-        // check(generatedIds, "L1_S2__S2_S3__S3_S1", "Z6.1");
-        // check(generatedIds, "L1_S2__L2_S3__S3_S1", "Z6.2");
-        // check(generatedIds, "L1_L2__S2_S3__S3_S1", "Z6.3");
-        // check(generatedIds, "S1_L2__S2_L3__S3_S1", "Z6.4");
-        // check(generatedIds, "S1_L2__S2_S3__S3_S1", "Z6.5");
-        // check(generatedIds, "S1_S2__S2_S3__S3_S1", "3.2W");
+        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");
@@ -258,6 +241,14 @@
         check(generatedIds, "S1_L2__S2_L3__S3_L1", "3.SB");
 
         check(generatedIds, "L1_L2__S2_L3__S3_S1", "W+RWC");
+
+        check(generatedIds, "L1_S2__S2_L3__S3_S1", "Z6.0");
+        check(generatedIds, "L1_S2__S2_S3__S3_S1", "Z6.1");
+        check(generatedIds, "L1_S2__L2_S3__S3_S1", "Z6.2");
+        check(generatedIds, "L1_L2__S2_S3__S3_S1", "Z6.3");
+        check(generatedIds, "S1_L2__S2_L3__S3_S1", "Z6.4");
+        check(generatedIds, "S1_L2__S2_S3__S3_S1", "Z6.5");
+        check(generatedIds, "S1_S2__S2_S3__S3_S1", "3.2W");
     }
 
     private void check(Set<String> ids, String id, String info) {
@@ -266,12 +257,12 @@
         }
     }
 
-    private void emit(MultiThread mt, List<String> scResults) {
+    private void emit(MultiThread mt, Collection<TraceResult> scResults) {
         String pathname = Utils.ensureDir(srcDir + "/" + pkg.replaceAll("\\.", "/"));
 
         String klass = mt.canonicalId() + "_Test";
 
-        Class[] klasses = new Class[mt.loadCount()];
+        Class[] klasses = new Class[mt.loadCount() + mt.allVariables().size()];
         for (int c = 0; c < klasses.length; c++) {
             klasses[c] = int.class;
         }
@@ -294,8 +285,16 @@
         pw.println();
         pw.println("@JCStressTest");
         pw.println("@Outcome(id = {");
-        for (String r : scResults) {
-            pw.println("            \"" + r + "\",");
+
+        for (TraceResult r : scResults) {
+            List<String> mappedValues = new ArrayList<>();
+            for (Value v : r.getResults().values()) {
+                mappedValues.add(v.toString());
+            }
+            for (Value v : r.getVars().values()) {
+                mappedValues.add(v.toString());
+            }
+            pw.println("            \"" + mappedValues.toString() + "\",");
         }
         pw.println("}, expect = Expect.ACCEPTABLE, desc = \"Sequential consistency.\")");
 
@@ -355,6 +354,16 @@
             pw.println();
         }
 
+        pw.println("    @Arbiter");
+        pw.println("    public void arbiter(" + resultName + " r) {");
+        int idx = mt.loadCount() + 1;
+        for (Integer varId : mt.allVariables()) {
+            pw.println("        r.r" + idx + " = x" + varId + ";");
+            idx++;
+        }
+        pw.println("    }");
+        pw.println();
+
         pw.println("}");
 
         pw.close();
--- a/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Trace.java	Mon May 23 14:03:36 2016 +0300
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/Trace.java	Mon May 23 17:12:38 2016 +0300
@@ -64,7 +64,7 @@
         return ops.size();
     }
 
-    public SortedMap<Result, Value> interpret() {
+    public TraceResult interpret() {
         int vars = 0;
         for (Op op : ops) {
             vars = Math.max(vars, op.getVarId());
@@ -91,7 +91,7 @@
             }
         }
 
-        return resValues;
+        return new TraceResult(resValues, values);
     }
 
     public Trace removeFirst() {
@@ -213,6 +213,24 @@
         return loads.equals(stores);
     }
 
+    public boolean matchedLoads() {
+        Set<Integer> loads = new HashSet<>();
+        Set<Integer> stores = new HashSet<>();
+        for (Op op : ops) {
+            switch (op.getType()) {
+                case STORE:
+                    stores.add(op.getVarId());
+                    loads.add(op.getVarId());
+                    break;
+                case LOAD:
+                    loads.add(op.getVarId());
+                    break;
+            }
+        }
+
+        return loads.equals(stores);
+    }
+
     public void assignResults() {
         int valId = Value.initial();
         int resId = 1;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/jcstress-test-gen/src/main/java/org/openjdk/jcstress/generator/seqcst/TraceResult.java	Mon May 23 17:12:38 2016 +0300
@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) 2014, 2015, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+package org.openjdk.jcstress.generator.seqcst;
+
+import java.util.Map;
+
+public class TraceResult {
+
+    private final Map<Result, Value> results;
+    private final Map<Integer, Value> vars;
+
+    public TraceResult(Map<Result, Value> results, Map<Integer, Value> vars) {
+        this.results = results;
+        this.vars = vars;
+    }
+
+    public Map<Result, Value> getResults() {
+        return results;
+    }
+
+    public Map<Integer, Value> getVars() {
+        return vars;
+    }
+
+    @Override
+    public String toString() {
+        return "{Results: " + results + ", Variables: " + vars + "}";
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+
+        TraceResult that = (TraceResult) o;
+
+        if (!results.equals(that.results)) return false;
+        return vars.equals(that.vars);
+
+    }
+
+    @Override
+    public int hashCode() {
+        int result = results.hashCode();
+        result = 31 * result + vars.hashCode();
+        return result;
+    }
+}