From 590db3c8af639f3ac0c59507d86cbbc95ecc2262 Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 12:29:04 -0400 Subject: [PATCH 1/3] Generalize Peterson invariant to N threads and add DSL local arrays - Generalize mutual_exclusion_peterson invariant to N threads (N >= 2) with cs_pcs array while maintaining backward compatibility with 2-thread thread0_cs_pc/thread1_cs_pc parameters. - Implement Mini-Spec 15.01 adding DSL local array support: - LocalDecl with INT_ARRAY support and arrayInit. - Lhs.LocalArrayLhs for local.arr[idx] assignments. - Parsing, type checking, and expression evaluation for local.arr[idx]. - DynamicState storage, indexing, copying, equality, hashing, and encoding for int[] locals. - MemoryLocation footprint derivation (t.arr[] vs t.arr) in step reads/writes. - End-to-end tests for Peterson N-thread invariant and DSL local array execution. Co-authored-by: Codex --- .../interleave/format/ProgramLoader.java | 27 +- .../interleave/format/dsl/DslLoader.java | 30 +- .../interleave/format/dsl/DynamicState.java | 95 ++++++- .../interleave/format/dsl/DynamicStep.java | 18 +- .../interleave/format/dsl/Evaluator.java | 15 +- .../format/dsl/ExpressionReads.java | 8 +- .../dev/samhb/interleave/format/dsl/Lhs.java | 8 +- .../interleave/format/dsl/LocalDecl.java | 57 +++- .../samhb/interleave/format/dsl/Parser.java | 18 +- .../interleave/format/dsl/TypeChecker.java | 11 +- .../format/registry/InvariantRegistry.java | 37 ++- .../format/InvariantRegistryTest.java | 57 ++++ .../interleave/format/ProgramLoaderTest.java | 42 +++ .../format/dsl/DslLocalArrayTest.java | 261 ++++++++++++++++++ .../dsl/DslPropertyObservationTest.java | 8 +- .../state/StateEncodingFidelityTest.java | 18 ++ 16 files changed, 664 insertions(+), 46 deletions(-) create mode 100644 src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java diff --git a/src/main/java/dev/samhb/interleave/format/ProgramLoader.java b/src/main/java/dev/samhb/interleave/format/ProgramLoader.java index 50eb960..68ddb56 100644 --- a/src/main/java/dev/samhb/interleave/format/ProgramLoader.java +++ b/src/main/java/dev/samhb/interleave/format/ProgramLoader.java @@ -274,11 +274,28 @@ private BenchmarkProgram load(ProgramDefinition def) { String invariantType = def.invariant().get("type").getAsString(); invariantRegistry.validateCompatibility(invariantType, def.state().get("type").getAsString()); - // mutual_exclusion_peterson requires exactly two threads - if ("mutual_exclusion_peterson".equals(invariantType) && threadDefs.size() != 2) { - throw new RegistryException( - "Invariant 'mutual_exclusion_peterson' requires exactly two threads" - ); + // mutual_exclusion_peterson requires at least two threads + if ("mutual_exclusion_peterson".equals(invariantType)) { + if (threadDefs.size() < 2) { + throw new RegistryException( + "Invariant 'mutual_exclusion_peterson' requires at least two threads" + ); + } + JsonObject invJson = def.invariant(); + if (invJson.has("cs_pcs")) { + if (invJson.get("cs_pcs").isJsonArray()) { + int csPcsLen = invJson.getAsJsonArray("cs_pcs").size(); + if (csPcsLen != threadDefs.size()) { + throw new RegistryException( + "Invariant 'cs_pcs' length (" + csPcsLen + ") must match thread count (" + threadDefs.size() + ")" + ); + } + } + } else if (threadDefs.size() != 2) { + throw new RegistryException( + "Invariant 'mutual_exclusion_peterson' requires two threads when using thread0_cs_pc/thread1_cs_pc; use 'cs_pcs' for N threads" + ); + } } invariant = invariantRegistry.create(def.invariant()); diff --git a/src/main/java/dev/samhb/interleave/format/dsl/DslLoader.java b/src/main/java/dev/samhb/interleave/format/dsl/DslLoader.java index ab46c68..8e90abe 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/DslLoader.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/DslLoader.java @@ -134,6 +134,7 @@ public static BenchmarkProgram load(ProgramDefinition def) { } else if (lhs instanceof Lhs.LocalLhs ll) { LocalDecl ld = decl.findLocal(ll.name()); if (ld == null) throw new RegistryException("Unknown local '" + ll.name() + "' at " + path + ".effects[" + eIdx + "]"); + if (ld.type() == FieldType.INT_ARRAY) throw new RegistryException("Local array '" + ll.name() + "' requires index: use local." + ll.name() + "[expr] at " + path + ".effects[" + eIdx + "]"); if (ld.type() != rhsType) throw new RegistryException("Type mismatch at " + path + ".effects[" + eIdx + "]: local '" + ll.name() + "' is " + ld.type() + ", rhs is " + rhsType); } else if (lhs instanceof Lhs.ArrayLhs al) { FieldDecl fd = decl.findField(al.arrayName()); @@ -152,6 +153,21 @@ public static BenchmarkProgram load(ProgramDefinition def) { totalNodes += n; if (totalNodes > 5000) throw new RegistryException("Total AST node count exceeds 5000"); // also check depth for index + } else if (lhs instanceof Lhs.LocalArrayLhs lal) { + LocalDecl ld = decl.findLocal(lal.localName()); + if (ld == null || ld.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown local array '" + lal.localName() + "' at " + path + ".effects[" + eIdx + "]"); + if (rhsType != FieldType.INT) throw new RegistryException("Array element assignment requires int at " + path + ".effects[" + eIdx + "]"); + try { + TypeChecker.requireInt(lal.index(), decl); + } catch (RegistryException ex) { + throw new RegistryException("Array index must be int at " + path + ".effects[" + eIdx + "]: " + ex.getMessage(), ex); + } + int d = Expr.depth(lal.index()); + int n = Expr.nodeCount(lal.index()); + if (d > 16) throw new RegistryException("Expression depth exceeds 16 at " + path + ".effects[" + eIdx + "] lhs index"); + if (n > 5000) throw new RegistryException("Expression nodes exceed bound at " + path + ".effects[" + eIdx + "]"); + totalNodes += n; + if (totalNodes > 5000) throw new RegistryException("Total AST node count exceeds 5000"); } int d = Expr.depth(rhs); int n = Expr.nodeCount(rhs); @@ -434,8 +450,18 @@ private static StateDecl parseStateDecl(JsonObject stateJson) { if (!initEl.isJsonPrimitive() || !initEl.getAsJsonPrimitive().isBoolean()) throw new RegistryException("'init' must be bool at " + path); ld = LocalDecl.ofBool(name, initEl.getAsBoolean()); } - case "int[]" -> throw new RegistryException("Local type 'int[]' not allowed at " + path + ".type"); - default -> throw new RegistryException("Unknown local type '" + typeStr + "' at " + path + ".type (valid: int, bool)"); + case "int[]" -> { + if (!initEl.isJsonArray()) throw new RegistryException("'init' must be array at " + path); + JsonArray arr = initEl.getAsJsonArray(); + if (arr.size() > 64) throw new RegistryException("Array length must be <=64 at " + path); + int[] vals = new int[arr.size()]; + for (int k = 0; k < arr.size(); k++) { + if (!arr.get(k).isJsonPrimitive() || !arr.get(k).getAsJsonPrimitive().isNumber()) throw new RegistryException("Array element must be int at " + path + ".init[" + k + "]"); + vals[k] = parseStrictInt(arr.get(k), path + ".init[" + k + "]"); + } + ld = LocalDecl.ofArray(name, vals); + } + default -> throw new RegistryException("Unknown local type '" + typeStr + "' at " + path + ".type (valid: int, bool, int[])"); } for (String k : o.keySet()) if (!k.equals("name") && !k.equals("type") && !k.equals("init")) throw new RegistryException("Unknown field '" + k + "' at " + path); locals.add(ld); diff --git a/src/main/java/dev/samhb/interleave/format/dsl/DynamicState.java b/src/main/java/dev/samhb/interleave/format/dsl/DynamicState.java index 98cfaef..e550609 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/DynamicState.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/DynamicState.java @@ -69,7 +69,13 @@ public DynamicState(StateDecl decl, int threadCount) { for (int tid = 0; tid < threadCount; tid++) { for (int j = 0; j < decl.locals().size(); j++) { LocalDecl l = decl.locals().get(j); - localValues[tid][j] = l.type() == FieldType.INT ? l.intInit() : l.boolInit(); + if (l.type() == FieldType.INT) { + localValues[tid][j] = l.intInit(); + } else if (l.type() == FieldType.BOOL) { + localValues[tid][j] = l.boolInit(); + } else { + localValues[tid][j] = Arrays.copyOf(l.arrayInit(), l.arrayInit().length); + } } } } @@ -235,6 +241,44 @@ public void setLocalBool(int tid, String name, boolean value) { localValues[tid][idx] = value; } + /** + * Returns a copy of a thread's declared {@code INT_ARRAY} local. + * + * @param tid the thread id + * @param name the declared local name + * @return copy of the array + */ + public int[] getLocalArray(int tid, String name) { + int idx = indexOfLocal(name); + int[] arr = (int[]) localValues[tid][idx]; + return Arrays.copyOf(arr, arr.length); + } + + /** + * Returns direct array reference for internal use (no copy). + * + * @param tid the thread id + * @param name the declared local name + * @return array reference + */ + int[] getLocalArrayRef(int tid, String name) { + int idx = indexOfLocal(name); + return (int[]) localValues[tid][idx]; + } + + /** + * Sets a thread's local array element. + * + * @param tid the thread id + * @param name the declared local name + * @param index element index + * @param value value to set + */ + public void setLocalArrayElement(int tid, String name, int index, int value) { + int[] arr = getLocalArrayRef(tid, name); + arr[index] = value; + } + /** * Resolves a declared field name to its storage index. * @@ -280,7 +324,11 @@ public SharedState deepCopy() { } Object[][] localCopy = new Object[threadCount][decl.locals().size()]; for (int tid = 0; tid < threadCount; tid++) { - localCopy[tid] = Arrays.copyOf(localValues[tid], localValues[tid].length); + for (int j = 0; j < decl.locals().size(); j++) { + Object lv = localValues[tid][j]; + if (lv instanceof int[] arr) localCopy[tid][j] = Arrays.copyOf(arr, arr.length); + else localCopy[tid][j] = lv; + } } return new DynamicState(decl, threadCount, fieldCopy, localCopy); } @@ -340,6 +388,13 @@ public void encodeTo(DataOutput out) throws IOException { out.writeInt(l.type().ordinal()); out.writeInt(l.intInit()); out.writeBoolean(l.boolInit()); + int[] init = l.arrayInit(); + if (init == null) { + out.writeInt(-1); + } else { + out.writeInt(init.length); + for (int v : init) out.writeInt(v); + } } // fields in declaration order: type ordinal, then value @@ -360,8 +415,15 @@ public void encodeTo(DataOutput out) throws IOException { for (int tid = 0; tid < threadCount; tid++) { for (int j = 0; j < decl.locals().size(); j++) { LocalDecl l = decl.locals().get(j); - if (l.type() == FieldType.INT) out.writeInt((Integer) localValues[tid][j]); - else out.writeBoolean((Boolean) localValues[tid][j]); + if (l.type() == FieldType.INT) { + out.writeInt((Integer) localValues[tid][j]); + } else if (l.type() == FieldType.BOOL) { + out.writeBoolean((Boolean) localValues[tid][j]); + } else { + int[] arr = (int[]) localValues[tid][j]; + out.writeInt(arr.length); + for (int v : arr) out.writeInt(v); + } } } } @@ -393,11 +455,14 @@ public boolean equals(Object o) { } else if (!a.equals(b)) return false; } for (int tid = 0; tid < threadCount; tid++) { - if (!Arrays.equals(localValues[tid], that.localValues[tid])) { - // need deep equals for possibly int[]? locals are scalar only, so direct equals - boolean eq = true; - for (int j = 0; j < localValues[tid].length; j++) if (!localValues[tid][j].equals(that.localValues[tid][j])) eq = false; - if (!eq) return false; + for (int j = 0; j < localValues[tid].length; j++) { + Object a = localValues[tid][j]; + Object b = that.localValues[tid][j]; + if (a instanceof int[] arrA && b instanceof int[] arrB) { + if (!Arrays.equals(arrA, arrB)) return false; + } else if (!a.equals(b)) { + return false; + } } } return true; @@ -418,7 +483,12 @@ public int hashCode() { if (v instanceof int[] arr) h = h * 31 + Arrays.hashCode(arr); else h = h * 31 + v.hashCode(); } - for (Object[] row : localValues) h = h * 31 + Arrays.hashCode(row); + for (Object[] row : localValues) { + for (Object v : row) { + if (v instanceof int[] arr) h = h * 31 + Arrays.hashCode(arr); + else h = h * 31 + v.hashCode(); + } + } return h; } @@ -448,7 +518,10 @@ public String toString() { for (int tid = 0; tid < threadCount; tid++) { for (int j = 0; j < decl.locals().size(); j++) { LocalDecl l = decl.locals().get(j); - sb.append("t").append(tid).append(".").append(l.name()).append("=").append(localValues[tid][j]); + sb.append("t").append(tid).append(".").append(l.name()).append("="); + Object lv = localValues[tid][j]; + if (lv instanceof int[] arr) sb.append(Arrays.toString(arr)); + else sb.append(lv); if (tid != threadCount - 1 || j != decl.locals().size() - 1) sb.append(", "); } } diff --git a/src/main/java/dev/samhb/interleave/format/dsl/DynamicStep.java b/src/main/java/dev/samhb/interleave/format/dsl/DynamicStep.java index ce50dcb..f0b3def 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/DynamicStep.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/DynamicStep.java @@ -55,6 +55,7 @@ public DynamicStep(int owner, Expr guard, List effects, StateDecl decl, ExpressionReads.collect(e.rhs(), owner, r); // lhs index reads for array if (e.lhs() instanceof Lhs.ArrayLhs al) ExpressionReads.collect(al.index(), owner, r); + if (e.lhs() instanceof Lhs.LocalArrayLhs lal) ExpressionReads.collect(lal.index(), owner, r); } // Property observations are separate; step footprints describe execution and enabledness. this.reads = Set.copyOf(r); @@ -76,6 +77,9 @@ private void addWrite(Lhs lhs, Set w) { else if (lhs instanceof Lhs.ArrayLhs al) { if (al.index() instanceof Expr.IntLit lit) w.add(MemoryLocation.of(al.arrayName() + "[" + lit.value() + "]")); else w.add(MemoryLocation.of(al.arrayName())); + } else if (lhs instanceof Lhs.LocalArrayLhs lal) { + if (lal.index() instanceof Expr.IntLit lit) w.add(MemoryLocation.of("t" + owner + "." + lal.localName() + "[" + lit.value() + "]")); + else w.add(MemoryLocation.of("t" + owner + "." + lal.localName())); } } @@ -172,10 +176,10 @@ public StepOutcome execute(SharedState state) { if (ld.type() == FieldType.INT) { if (rhsVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED; ds.setLocalInt(owner, ll.name(), rhsVal.asInt()); - } else { + } else if (ld.type() == FieldType.BOOL) { if (rhsVal.type() != FieldType.BOOL) return StepOutcome.ASSERTION_FAILED; ds.setLocalBool(owner, ll.name(), rhsVal.asBool()); - } + } else return StepOutcome.ASSERTION_FAILED; } else if (lhs instanceof Lhs.ArrayLhs al) { FieldDecl fd = decl.findField(al.arrayName()); if (fd == null || fd.type() != FieldType.INT_ARRAY) return StepOutcome.ASSERTION_FAILED; @@ -186,6 +190,16 @@ public StepOutcome execute(SharedState state) { int[] arr = ds.getArrayRef(al.arrayName()); if (idx < 0 || idx >= arr.length) return StepOutcome.ASSERTION_FAILED; arr[idx] = rhsVal.asInt(); + } else if (lhs instanceof Lhs.LocalArrayLhs lal) { + LocalDecl ld = decl.findLocal(lal.localName()); + if (ld == null || ld.type() != FieldType.INT_ARRAY) return StepOutcome.ASSERTION_FAILED; + if (rhsVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED; + Evaluator.Value idxVal = Evaluator.eval(lal.index(), ds, owner); + if (idxVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED; + int idx = idxVal.asInt(); + int[] arr = ds.getLocalArrayRef(owner, lal.localName()); + if (idx < 0 || idx >= arr.length) return StepOutcome.ASSERTION_FAILED; + arr[idx] = rhsVal.asInt(); } } return StepOutcome.ADVANCED; diff --git a/src/main/java/dev/samhb/interleave/format/dsl/Evaluator.java b/src/main/java/dev/samhb/interleave/format/dsl/Evaluator.java index 1ca25c3..5269116 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/Evaluator.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/Evaluator.java @@ -113,13 +113,20 @@ public static Value eval(Expr expr, DynamicState state, int tid) { LocalDecl ld = state.decl().findLocal(l.name()); if (ld == null) throw new RegistryException("Unknown local '" + l.name() + "'"); if (ld.type() == FieldType.INT) return new IntVal(state.getLocalInt(tid, l.name())); - return new BoolVal(state.getLocalBool(tid, l.name())); + if (ld.type() == FieldType.BOOL) return new BoolVal(state.getLocalBool(tid, l.name())); + throw new RegistryException("Local '" + l.name() + "' is array; use local." + l.name() + "[index]"); } if (expr instanceof Expr.ArrayAccess a) { - // local array access is not allowed (locals scalar only) — will have been rejected at type-check, - // but handle "local.name" case for robustness if (a.arrayName().startsWith("local.")) { - throw new EvalException("Local array access not supported: " + a.arrayName()); + String localName = a.arrayName().substring("local.".length()); + LocalDecl ld = state.decl().findLocal(localName); + if (ld == null || ld.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown local array '" + localName + "'"); + Value idxVal = eval(a.index(), state, tid); + if (idxVal.type() != FieldType.INT) throw new RegistryException("Array index must be int"); + int idx = idxVal.asInt(); + int[] arr = state.getLocalArrayRef(tid, localName); + if (idx < 0 || idx >= arr.length) throw new EvalException("Array index out of bounds: " + a.arrayName() + "[" + idx + "] length " + arr.length); + return new IntVal(arr[idx]); } FieldDecl f = state.decl().findField(a.arrayName()); if (f == null || f.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown array field '" + a.arrayName() + "'"); diff --git a/src/main/java/dev/samhb/interleave/format/dsl/ExpressionReads.java b/src/main/java/dev/samhb/interleave/format/dsl/ExpressionReads.java index 1096541..3e3a251 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/ExpressionReads.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/ExpressionReads.java @@ -20,7 +20,13 @@ static void collect(Expr expr, int owner, Set out) { else if (expr instanceof Expr.LocalRef l) out.add(MemoryLocation.of("t" + owner + "." + l.name())); else if (expr instanceof Expr.ArrayAccess a) { if (a.arrayName().startsWith("local.")) { - out.add(MemoryLocation.of("t" + owner + "." + a.arrayName().substring(6))); + String localName = a.arrayName().substring("local.".length()); + if (a.index() instanceof Expr.IntLit literal) { + out.add(MemoryLocation.of("t" + owner + "." + localName + "[" + literal.value() + "]")); + } else { + out.add(MemoryLocation.of("t" + owner + "." + localName)); + collect(a.index(), owner, out); + } } else if (a.index() instanceof Expr.IntLit literal) { out.add(MemoryLocation.of(a.arrayName() + "[" + literal.value() + "]")); } else { diff --git a/src/main/java/dev/samhb/interleave/format/dsl/Lhs.java b/src/main/java/dev/samhb/interleave/format/dsl/Lhs.java index 8c12546..ff02841 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/Lhs.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/Lhs.java @@ -4,7 +4,7 @@ /** * Left-hand side of an effect assignment. */ -public sealed interface Lhs permits Lhs.FieldLhs, Lhs.LocalLhs, Lhs.ArrayLhs { +public sealed interface Lhs permits Lhs.FieldLhs, Lhs.LocalLhs, Lhs.ArrayLhs, Lhs.LocalArrayLhs { /** * Shared field scalar assignment. * @param name declared field or local name @@ -21,4 +21,10 @@ record LocalLhs(String name) implements Lhs {} * @param index expression selecting an array element */ record ArrayLhs(String arrayName, Expr index) implements Lhs {} + /** + * Per-thread local array element assignment. + * @param localName declared per-thread local array name + * @param index expression selecting an array element + */ + record LocalArrayLhs(String localName, Expr index) implements Lhs {} } diff --git a/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java b/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java index e26b2e3..b56abeb 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java @@ -1,15 +1,35 @@ /** Per-thread local declaration for declarative state. */ package dev.samhb.interleave.format.dsl; +import java.util.Arrays; +import java.util.Objects; + /** * Per-thread local declaration for declarative state. * * @param name local name, matches [a-z][a-z0-9_]* - * @param type local type (INT or BOOL only) + * @param type local type (INT, BOOL, or INT_ARRAY) * @param intInit initial int value * @param boolInit initial bool value + * @param arrayInit initial array contents (for INT_ARRAY), defensive copy on construction */ -public record LocalDecl(String name, FieldType type, int intInit, boolean boolInit) { +public record LocalDecl(String name, FieldType type, int intInit, boolean boolInit, int[] arrayInit) { + /** + * Compact constructor: defensive copy of array init to preserve immutability. + */ + public LocalDecl { + if (arrayInit != null) arrayInit = Arrays.copyOf(arrayInit, arrayInit.length); + } + + /** + * Returns a defensive copy of declared initial array contents. + * @return fresh copy or null + */ + @Override + public int[] arrayInit() { + return arrayInit == null ? null : Arrays.copyOf(arrayInit, arrayInit.length); + } + /** * Creates local for int. * @@ -18,7 +38,7 @@ public record LocalDecl(String name, FieldType type, int intInit, boolean boolIn * @return decl */ public static LocalDecl ofInt(String name, int init) { - return new LocalDecl(name, FieldType.INT, init, false); + return new LocalDecl(name, FieldType.INT, init, false, null); } /** @@ -29,6 +49,35 @@ public static LocalDecl ofInt(String name, int init) { * @return decl */ public static LocalDecl ofBool(String name, boolean init) { - return new LocalDecl(name, FieldType.BOOL, 0, init); + return new LocalDecl(name, FieldType.BOOL, 0, init, null); + } + + /** + * Creates local for int array. + * + * @param name local name + * @param init initial contents + * @return decl + */ + public static LocalDecl ofArray(String name, int[] init) { + return new LocalDecl(name, FieldType.INT_ARRAY, 0, false, init); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (!(o instanceof LocalDecl that)) return false; + return intInit == that.intInit + && boolInit == that.boolInit + && Objects.equals(name, that.name) + && type == that.type + && Arrays.equals(arrayInit, that.arrayInit); + } + + @Override + public int hashCode() { + int result = Objects.hash(name, type, intInit, boolInit); + result = 31 * result + Arrays.hashCode(arrayInit); + return result; } } diff --git a/src/main/java/dev/samhb/interleave/format/dsl/Parser.java b/src/main/java/dev/samhb/interleave/format/dsl/Parser.java index d7df07f..10d9c43 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/Parser.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/Parser.java @@ -135,10 +135,20 @@ private int findTopLevelEquals() { private Lhs parseLhs(String s) { s = s.trim(); if (s.startsWith("local.")) { - String name = s.substring(6).trim(); - if (name.contains("[") || name.contains("]")) throw new RegistryException("Local lhs must not have array index: '" + s + "'"); - validateIdent(name); - return new Lhs.LocalLhs(name); + String rest = s.substring(6).trim(); + int lb = rest.indexOf('['); + if (lb >= 0) { + int rb = rest.lastIndexOf(']'); + if (rb < 0 || rb != rest.length() - 1) throw new RegistryException("Invalid local array lhs: '" + s + "'"); + String name = rest.substring(0, lb).trim(); + String idxStr = rest.substring(lb + 1, rb).trim(); + validateIdent(name); + if (idxStr.isEmpty()) throw new RegistryException("Array index empty: '" + s + "'"); + Expr idx = new Parser(idxStr).parseExpr(); + return new Lhs.LocalArrayLhs(name, idx); + } + validateIdent(rest); + return new Lhs.LocalLhs(rest); } // check array lhs int lb = s.indexOf('['); diff --git a/src/main/java/dev/samhb/interleave/format/dsl/TypeChecker.java b/src/main/java/dev/samhb/interleave/format/dsl/TypeChecker.java index 2b50317..55c426f 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/TypeChecker.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/TypeChecker.java @@ -31,10 +31,19 @@ public static FieldType check(Expr expr, StateDecl decl) { if (expr instanceof Expr.LocalRef l) { LocalDecl ld = decl.findLocal(l.name()); if (ld == null) throw new RegistryException("Unknown local '" + l.name() + "'"); + if (ld.type() == FieldType.INT_ARRAY) throw new RegistryException("Local array '" + l.name() + "' cannot be used as scalar: use local." + l.name() + "[index]"); return ld.type(); } if (expr instanceof Expr.ArrayAccess a) { - if (a.arrayName().startsWith("local.")) throw new RegistryException("Local array access not supported: " + a.arrayName()); + if (a.arrayName().startsWith("local.")) { + String locName = a.arrayName().substring(6); + LocalDecl ld = decl.findLocal(locName); + if (ld == null) throw new RegistryException("Unknown local array '" + locName + "'"); + if (ld.type() != FieldType.INT_ARRAY) throw new RegistryException("Local '" + locName + "' is not an array"); + FieldType idxT = check(a.index(), decl); + if (idxT != FieldType.INT) throw new RegistryException("Array index must be int"); + return FieldType.INT; + } FieldDecl f = decl.findField(a.arrayName()); if (f == null) throw new RegistryException("Unknown array field '" + a.arrayName() + "'"); if (f.type() != FieldType.INT_ARRAY) throw new RegistryException("Field '" + a.arrayName() + "' is not an array"); diff --git a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java index eaf70df..91a4ea7 100644 --- a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java +++ b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java @@ -35,17 +35,40 @@ public InvariantRegistry() { /** Registers the supported built-in factories by their declarative names. */ private void registerBuiltins() { - // mutual_exclusion_peterson: thread0_cs_pc, thread1_cs_pc + // mutual_exclusion_peterson: cs_pcs (array of int) or thread0_cs_pc, thread1_cs_pc register("mutual_exclusion_peterson", Set.of("peterson"), json -> { - int t0Pc = JsonHelper.getInt(json, "thread0_cs_pc", "mutual_exclusion_peterson"); - int t1Pc = JsonHelper.getInt(json, "thread1_cs_pc", "mutual_exclusion_peterson"); + int[] csPcs; + if (json.has("cs_pcs")) { + com.google.gson.JsonArray arr = JsonHelper.getArray(json, "cs_pcs", "mutual_exclusion_peterson"); + if (arr.size() < 2) { + throw new RegistryException("Parameter 'cs_pcs' for mutual_exclusion_peterson must have at least 2 entries"); + } + csPcs = new int[arr.size()]; + for (int i = 0; i < arr.size(); i++) { + com.google.gson.JsonElement el = arr.get(i); + if (!el.isJsonPrimitive() || !el.getAsJsonPrimitive().isNumber()) { + throw new RegistryException("Entry in 'cs_pcs' must be an integer at index " + i); + } + csPcs[i] = el.getAsInt(); + } + } else { + int t0Pc = JsonHelper.getInt(json, "thread0_cs_pc", "mutual_exclusion_peterson"); + int t1Pc = JsonHelper.getInt(json, "thread1_cs_pc", "mutual_exclusion_peterson"); + csPcs = new int[]{t0Pc, t1Pc}; + } return (state, config) -> { PetersonState ps = (PetersonState) state; List pcs = config.programCounters(); - boolean bothFlagsTrue = ps.flag(0) && ps.flag(1); - boolean t0InCsZone = pcs.get(0) >= t0Pc; - boolean t1InCsZone = pcs.get(1) >= t1Pc; - return !(bothFlagsTrue && t0InCsZone && t1InCsZone); + int inCs = 0; + for (int i = 0; i < csPcs.length; i++) { + if (i < pcs.size() && ps.flag(i) && pcs.get(i) >= csPcs[i]) { + inCs++; + if (inCs > 1) { + return false; + } + } + } + return true; }; }, "peterson"); diff --git a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java index 3a75772..7c9fc2b 100644 --- a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java +++ b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java @@ -104,6 +104,63 @@ void mutualExclusionPeterson_holds_whenBothFlagsTrueButNotBothInCS() { assertFalse(invariant.holds(after.state(), after), "the CS zone includes counters past its boundary"); } + @Test + void mutualExclusionPeterson_csPcs_validation() { + var notArr = new com.google.gson.JsonObject(); + notArr.addProperty("type", "mutual_exclusion_peterson"); + notArr.addProperty("cs_pcs", 123); + RegistryException ex1 = assertThrows(RegistryException.class, () -> registry.create(notArr)); + assertTrue(ex1.getMessage().contains("must be an array")); + + var tooShort = new com.google.gson.JsonObject(); + tooShort.addProperty("type", "mutual_exclusion_peterson"); + var shortArr = new com.google.gson.JsonArray(); + shortArr.add(1); + tooShort.add("cs_pcs", shortArr); + RegistryException ex2 = assertThrows(RegistryException.class, () -> registry.create(tooShort)); + assertTrue(ex2.getMessage().contains("at least 2 entries")); + + var notNum = new com.google.gson.JsonObject(); + notNum.addProperty("type", "mutual_exclusion_peterson"); + var badArr = new com.google.gson.JsonArray(); + badArr.add(1); + badArr.add("not-a-number"); + notNum.add("cs_pcs", badArr); + RegistryException ex3 = assertThrows(RegistryException.class, () -> registry.create(notNum)); + assertTrue(ex3.getMessage().contains("must be an integer at index 1")); + } + + @Test + void mutualExclusionPeterson_threeThreads_withCsPcs() { + var json = new com.google.gson.JsonObject(); + json.addProperty("type", "mutual_exclusion_peterson"); + var arr = new com.google.gson.JsonArray(); + arr.add(2); + arr.add(2); + arr.add(2); + json.add("cs_pcs", arr); + Invariant invariant = registry.create(json); + + // PetersonState for 3 threads: flags [t0, t1, t2] + PetersonState sNone = PetersonState.of(new boolean[]{false, false, false}, 0); + Configuration cNone = Configuration.forTest(sNone, List.of(2, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); + assertTrue(invariant.holds(sNone, cNone)); + + PetersonState sOne = PetersonState.of(new boolean[]{true, false, false}, 0); + Configuration cOne = Configuration.forTest(sOne, List.of(2, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); + assertTrue(invariant.holds(sOne, cOne)); + + // Two in CS -> violation + PetersonState sTwo = PetersonState.of(new boolean[]{true, true, false}, 0); + Configuration cTwo = Configuration.forTest(sTwo, List.of(2, 2, 1), List.of(3, 3, 3), List.of(0, 1, 2)); + assertFalse(invariant.holds(sTwo, cTwo)); + + // All three in CS -> violation + PetersonState sThree = PetersonState.of(new boolean[]{true, true, true}, 0); + Configuration cThree = Configuration.forTest(sThree, List.of(2, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); + assertFalse(invariant.holds(sThree, cThree)); + } + @Test void counterEquals_holds_whenNotTerminated() { diff --git a/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java b/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java index a9b47f3..4e38129 100644 --- a/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java +++ b/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java @@ -343,6 +343,48 @@ void loadMutualExclusionPeterson_twoThreads_succeeds() { assertEquals("test", program.name()); } + @Test + /** Tests loadMutualExclusionPeterson_threeThreads_withCsPcs_succeeds. */ + void loadMutualExclusionPeterson_threeThreads_withCsPcs_succeeds() { + String json = """ + { + "format": "typed", + "name": "test-3t", + "state": {"type": "peterson", "flags": [false, false, false], "turn": 0}, + "threads": [ + {"id": 0, "steps": [{"type": "write_flag", "value": true}]}, + {"id": 1, "steps": [{"type": "write_flag", "value": true}]}, + {"id": 2, "steps": [{"type": "write_flag", "value": true}]} + ], + "invariant": {"type": "mutual_exclusion_peterson", "cs_pcs": [1, 1, 1]} + } + """; + BenchmarkProgram program = loader.load(json); + assertNotNull(program); + assertEquals("test-3t", program.name()); + } + + @Test + /** Tests loadMutualExclusionPeterson_csPcsLengthMismatch_throwsRegistryException. */ + void loadMutualExclusionPeterson_csPcsLengthMismatch_throwsRegistryException() { + String json = """ + { + "format": "typed", + "name": "test-mismatch", + "state": {"type": "peterson", "flags": [false, false, false], "turn": 0}, + "threads": [ + {"id": 0, "steps": [{"type": "write_flag", "value": true}]}, + {"id": 1, "steps": [{"type": "write_flag", "value": true}]}, + {"id": 2, "steps": [{"type": "write_flag", "value": true}]} + ], + "invariant": {"type": "mutual_exclusion_peterson", "cs_pcs": [1, 1]} + } + """; + RegistryException ex = assertThrows(dev.samhb.interleave.format.registry.RegistryException.class, + () -> loader.load(json)); + assertTrue(ex.getMessage().contains("must match thread count"), ex.getMessage()); + } + @Test /** Tests loadMissingState_throwsRegistryException. */ void loadMissingState_throwsRegistryException() { diff --git a/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java b/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java new file mode 100644 index 0000000..bd3cc2e --- /dev/null +++ b/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java @@ -0,0 +1,261 @@ +/** Tests for declarative DSL local array support. */ +package dev.samhb.interleave.format.dsl; + +import dev.samhb.interleave.bugs.BenchmarkProgram; +import dev.samhb.interleave.core.MemoryLocation; +import dev.samhb.interleave.core.StepOutcome; +import dev.samhb.interleave.format.ProgramLoader; +import dev.samhb.interleave.format.registry.RegistryException; +import dev.samhb.interleave.search.DfsExplorer; +import dev.samhb.interleave.search.DfsResult; +import dev.samhb.interleave.state.HashingStateStore; +import org.junit.jupiter.api.Test; + +import java.util.List; +import java.util.Set; + +import static org.junit.jupiter.api.Assertions.assertArrayEquals; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Tests parsing, type checking, runtime execution, and POR memory footprints for DSL local arrays. + */ +class DslLocalArrayTest { + + private final ProgramLoader loader = new ProgramLoader(); + + /** Tests valid declaration and execution of a program with local arrays. */ + @Test + void loadAndExecute_localArrayProgram_succeeds() { + String json = """ + { + "format": "declarative", + "name": "local-array-demo", + "state": { + "fields": [ + {"name": "done", "type": "bool", "init": false} + ], + "locals": [ + {"name": "items", "type": "int[]", "init": [10, 20, 30]}, + {"name": "idx", "type": "int", "init": 1} + ] + }, + "threads": [ + { + "id": 0, + "steps": [ + { + "name": "mutate-local", + "guard": "local.items[local.idx] == 20", + "effects": ["local.items[1] = 99", "done = true"] + } + ] + } + ] + } + """; + BenchmarkProgram prog = loader.load(json); + assertNotNull(prog); + + DfsExplorer explorer = new DfsExplorer(); + DfsResult result = explorer.explore(prog.program(), null, new HashingStateStore(), null); + assertNotNull(result); + assertEquals(2, result.statesExplored()); + } + + /** Tests thread isolation for local arrays. */ + @Test + void localArray_threadIsolation() { + StateDecl decl = new StateDecl( + List.of(FieldDecl.ofInt("shared", 0)), + List.of(LocalDecl.ofArray("buf", new int[]{1, 2, 3})) + ); + DynamicState state = new DynamicState(decl, 2); + + // Thread 0 modifies buf[0] + state.setLocalArrayElement(0, "buf", 0, 100); + + // Thread 1 buf must remain unchanged + assertEquals(100, state.getLocalArray(0, "buf")[0]); + assertEquals(1, state.getLocalArray(1, "buf")[0]); + assertArrayEquals(new int[]{100, 2, 3}, state.getLocalArray(0, "buf")); + assertArrayEquals(new int[]{1, 2, 3}, state.getLocalArray(1, "buf")); + } + + /** Tests memory footprint derivation for static and dynamic local array accesses. */ + @Test + void stepFootprint_localArrayReadsAndWrites() { + StateDecl decl = new StateDecl( + List.of(FieldDecl.ofInt("x", 0)), + List.of(LocalDecl.ofArray("buf", new int[]{0, 0}), LocalDecl.ofInt("i", 0)) + ); + + // Static index write: local.buf[1] = 5 + Effect effStatic = new Effect(new Lhs.LocalArrayLhs("buf", new Expr.IntLit(1)), new Expr.IntLit(5)); + DynamicStep stepStatic = new DynamicStep(0, null, List.of(effStatic), decl, "static-write"); + assertEquals(Set.of(MemoryLocation.of("t0.buf[1]")), stepStatic.writes()); + assertTrue(stepStatic.reads().isEmpty()); + + // Dynamic index write: local.buf[local.i] = 7 + Effect effDyn = new Effect(new Lhs.LocalArrayLhs("buf", new Expr.LocalRef("i")), new Expr.IntLit(7)); + DynamicStep stepDyn = new DynamicStep(0, null, List.of(effDyn), decl, "dyn-write"); + assertEquals(Set.of(MemoryLocation.of("t0.buf")), stepDyn.writes()); + assertEquals(Set.of(MemoryLocation.of("t0.i")), stepDyn.reads()); + + // Dynamic index read in guard: local.buf[local.i] > 0 + Expr guard = new Expr.BinaryOp(new Expr.ArrayAccess("local.buf", new Expr.LocalRef("i")), ">", new Expr.IntLit(0)); + DynamicStep stepGuard = new DynamicStep(0, guard, List.of(effStatic), decl, "guard-step"); + assertEquals(Set.of(MemoryLocation.of("t0.buf"), MemoryLocation.of("t0.i")), stepGuard.reads()); + } + + /** Tests runtime out-of-bounds error handling. */ + @Test + void outOfBounds_evaluatesToAssertionFailed() { + StateDecl decl = new StateDecl( + List.of(FieldDecl.ofInt("x", 0)), + List.of(LocalDecl.ofArray("buf", new int[]{10, 20})) + ); + DynamicState state = new DynamicState(decl, 1); + + // Guard OOB: enabled() returns true so execute() reports ASSERTION_FAILED + Expr oobGuard = new Expr.BinaryOp(new Expr.ArrayAccess("local.buf", new Expr.IntLit(5)), "==", new Expr.IntLit(10)); + Effect dummyEff = new Effect(new Lhs.FieldLhs("x"), new Expr.IntLit(1)); + DynamicStep stepGuard = new DynamicStep(0, oobGuard, List.of(dummyEff), decl, "oob-guard"); + assertTrue(stepGuard.enabled(state)); + assertEquals(StepOutcome.ASSERTION_FAILED, stepGuard.execute(state)); + + // Effect OOB write + Effect oobWrite = new Effect(new Lhs.LocalArrayLhs("buf", new Expr.IntLit(10)), new Expr.IntLit(99)); + DynamicStep stepWrite = new DynamicStep(0, null, List.of(oobWrite), decl, "oob-write"); + assertTrue(stepWrite.enabled(state)); + assertEquals(StepOutcome.ASSERTION_FAILED, stepWrite.execute(state)); + } + + /** Tests validation error on local array without index in expression. */ + @Test + void validation_localArrayWithoutIndexInExpr_throws() { + String json = """ + { + "format": "declarative", + "name": "bad-ref", + "state": { + "fields": [{"name": "x", "type": "int", "init": 0}], + "locals": [{"name": "arr", "type": "int[]", "init": [1, 2]}] + }, + "threads": [ + { + "id": 0, + "steps": [ + {"effects": ["x = local.arr"]} + ] + } + ] + } + """; + RegistryException ex = assertThrows(RegistryException.class, () -> loader.load(json)); + assertTrue(ex.getMessage().contains("cannot be used as scalar: use local.arr[index]")); + } + + /** Tests validation error on whole local array assignment. */ + @Test + void validation_localArrayWholeAssignment_throws() { + String json = """ + { + "format": "declarative", + "name": "bad-assign", + "state": { + "fields": [{"name": "x", "type": "int", "init": 0}], + "locals": [{"name": "arr", "type": "int[]", "init": [1, 2]}] + }, + "threads": [ + { + "id": 0, + "steps": [ + {"effects": ["local.arr = 5"]} + ] + } + ] + } + """; + RegistryException ex = assertThrows(RegistryException.class, () -> loader.load(json)); + assertTrue(ex.getMessage().contains("requires index: use local.arr[expr]")); + } + + /** Tests validation error on non-int assignment to local array element. */ + @Test + void validation_nonIntAssignToLocalArray_throws() { + String json = """ + { + "format": "declarative", + "name": "bad-type-assign", + "state": { + "fields": [{"name": "x", "type": "int", "init": 0}], + "locals": [{"name": "arr", "type": "int[]", "init": [1, 2]}] + }, + "threads": [ + { + "id": 0, + "steps": [ + {"effects": ["local.arr[0] = true"]} + ] + } + ] + } + """; + RegistryException ex = assertThrows(RegistryException.class, () -> loader.load(json)); + assertTrue(ex.getMessage().contains("requires int")); + } + + /** Tests validation error when local array is referenced in invariant. */ + @Test + void validation_localArrayInInvariant_throws() { + String json = """ + { + "format": "declarative", + "name": "bad-inv", + "state": { + "fields": [{"name": "x", "type": "int", "init": 0}], + "locals": [{"name": "arr", "type": "int[]", "init": [1, 2]}] + }, + "threads": [ + { + "id": 0, + "steps": [{"effects": ["x = 1"]}] + } + ], + "invariant": { + "expr": "local.arr[0] == 1" + } + } + """; + RegistryException ex = assertThrows(RegistryException.class, () -> loader.load(json)); + assertTrue(ex.getMessage().contains("Invariant must not reference local.*")); + } + + /** Tests local array init exceeding 64 elements limit. */ + @Test + void validation_localArrayTooLong_throws() { + StringBuilder sb = new StringBuilder("["); + for (int i = 0; i < 65; i++) { + if (i > 0) sb.append(", "); + sb.append("0"); + } + sb.append("]"); + String json = """ + { + "format": "declarative", + "name": "too-long", + "state": { + "fields": [{"name": "x", "type": "int", "init": 0}], + "locals": [{"name": "arr", "type": "int[]", "init": %s}] + }, + "threads": [{"id": 0, "steps": [{"effects": ["x = 1"]}]}] + } + """.formatted(sb.toString()); + RegistryException ex = assertThrows(RegistryException.class, () -> loader.load(json)); + assertTrue(ex.getMessage().contains("Array length must be <=64")); + } +} diff --git a/src/test/java/dev/samhb/interleave/format/dsl/DslPropertyObservationTest.java b/src/test/java/dev/samhb/interleave/format/dsl/DslPropertyObservationTest.java index 1dc8a84..aac311a 100644 --- a/src/test/java/dev/samhb/interleave/format/dsl/DslPropertyObservationTest.java +++ b/src/test/java/dev/samhb/interleave/format/dsl/DslPropertyObservationTest.java @@ -76,12 +76,12 @@ void runtimePredicateErrorsRemainViolations() { assertEquals(TraceOutcome.VIOLATION, result.traces().getFirst().outcome()); } - /** Verifies that local arrays are rejected before observation analysis. */ + /** Verifies that local arrays in invariants are rejected before observation analysis. */ @Test - void localArraysAreRejectedBeforeObservationAnalysis() { + void localArraysInInvariantsAreRejectedBeforeObservationAnalysis() { RegistryException error = assertThrows(RegistryException.class, () -> new ProgramLoader().load( - arrays("{\"when\":\"always\",\"expr\":\"x >= 0\"}", "x = local.r[idx]", "y = 1"))); - assertTrue(error.getMessage().contains("Local array access not supported")); + arrays("{\"when\":\"always\",\"expr\":\"local.arr[0] >= 0\"}", "x = 1", "y = 1"))); + assertTrue(error.getMessage().contains("Invariant must not reference local.*")); } /** Verifies that independent work reduces an eight thread grid to one schedule. */ diff --git a/src/test/java/dev/samhb/interleave/state/StateEncodingFidelityTest.java b/src/test/java/dev/samhb/interleave/state/StateEncodingFidelityTest.java index d8de257..4ba8c06 100644 --- a/src/test/java/dev/samhb/interleave/state/StateEncodingFidelityTest.java +++ b/src/test/java/dev/samhb/interleave/state/StateEncodingFidelityTest.java @@ -515,6 +515,24 @@ void encodeDynamicState_eachEncodedField_changesEncoding() { assertAllEncodingsDistinct("DynamicState mixed int and boolean locals", List.of(mixedBase, mixedIntSet, mixedBoolSet)); + // Local array branch: local INT_ARRAY values and mutations + StateDecl withArrayLocal = new StateDecl( + List.of(FieldDecl.ofInt("count", BASE_INT)), + List.of(LocalDecl.ofArray("arr", new int[]{1, 2, 3}))); + DynamicState arrayLocalBase = new DynamicState(withArrayLocal, 1); + DynamicState arrayLocalElemChanged = new DynamicState(withArrayLocal, 1); + arrayLocalElemChanged.setLocalArrayElement(0, "arr", 1, 99); + assertEncodingDiffers("localValues[arr] element changed", arrayLocalBase, arrayLocalElemChanged); + + StateDecl withShorterArrayLocal = new StateDecl( + List.of(FieldDecl.ofInt("count", BASE_INT)), + List.of(LocalDecl.ofArray("arr", new int[]{1, 2}))); + DynamicState shorterArrayLocal = new DynamicState(withShorterArrayLocal, 1); + assertEncodingDiffers("localValues[arr] length", arrayLocalBase, shorterArrayLocal); + + assertAllEncodingsDistinct("DynamicState local array variations", + List.of(arrayLocalBase, arrayLocalElemChanged, shorterArrayLocal)); + // Full integer spread on the local, not just the single 7 above. List locals = new ArrayList<>(); for (int value : INT_SPREAD) { From 41d2ee52d7e601e5f4c904d234ec9c083831d35e Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 16:30:34 -0400 Subject: [PATCH 2/3] Address CodeRabbit and Graphify review findings on PR 52 - LocalDecl: normalize null arrayInit to empty array and restore 4-arg constructor for backward compatibility. - InvariantRegistry: reject fractional/out-of-range cs_pcs entries using intValueExact and guard evaluation loop against bounds mismatches. - PetersonState: add threadCount() accessor. - InvariantRegistryTest & ProgramLoaderTest: document test contracts with Javadoc before annotations, verify fractional/overflow rejections, verify thread 2 involvement in Peterson violation, and verify loaded invariant evaluation. - DslLocalArrayTest: assert terminal state local-array contents via StateVisitor, test null initializer normalization, and improve Javadoc coverage. Co-authored-by: Codex --- .../samhb/interleave/core/PetersonState.java | 9 ++++ .../interleave/format/dsl/LocalDecl.java | 26 ++++++++-- .../format/registry/InvariantRegistry.java | 12 +++-- .../format/InvariantRegistryTest.java | 34 +++++++++++-- .../interleave/format/ProgramLoaderTest.java | 18 ++++++- .../format/dsl/DslLocalArrayTest.java | 48 +++++++++++++++---- 6 files changed, 126 insertions(+), 21 deletions(-) diff --git a/src/main/java/dev/samhb/interleave/core/PetersonState.java b/src/main/java/dev/samhb/interleave/core/PetersonState.java index 80ddebc..b3715db 100644 --- a/src/main/java/dev/samhb/interleave/core/PetersonState.java +++ b/src/main/java/dev/samhb/interleave/core/PetersonState.java @@ -59,6 +59,15 @@ public boolean flag(int threadId) { return flag[threadId]; } + /** + * Returns the number of threads modeled by this state. + * + * @return thread count + */ + public int threadCount() { + return flag.length; + } + /** * Updates flag in this mutable modeled state. * @param threadId zero-based modeled thread ID diff --git a/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java b/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java index b56abeb..2237a04 100644 --- a/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java +++ b/src/main/java/dev/samhb/interleave/format/dsl/LocalDecl.java @@ -15,10 +15,27 @@ */ public record LocalDecl(String name, FieldType type, int intInit, boolean boolInit, int[] arrayInit) { /** - * Compact constructor: defensive copy of array init to preserve immutability. + * Compact constructor: defensive copy of array init to preserve immutability, + * normalizing null to an empty array for INT_ARRAY type. */ public LocalDecl { - if (arrayInit != null) arrayInit = Arrays.copyOf(arrayInit, arrayInit.length); + if (arrayInit != null) { + arrayInit = Arrays.copyOf(arrayInit, arrayInit.length); + } else if (type == FieldType.INT_ARRAY) { + arrayInit = new int[0]; + } + } + + /** + * Backward-compatible 4-argument constructor for scalar locals. + * + * @param name local name + * @param type local type + * @param intInit initial int value + * @param boolInit initial bool value + */ + public LocalDecl(String name, FieldType type, int intInit, boolean boolInit) { + this(name, type, intInit, boolInit, null); } /** @@ -56,11 +73,12 @@ public static LocalDecl ofBool(String name, boolean init) { * Creates local for int array. * * @param name local name - * @param init initial contents + * @param init initial contents (copied, or normalized to empty array if null) * @return decl */ public static LocalDecl ofArray(String name, int[] init) { - return new LocalDecl(name, FieldType.INT_ARRAY, 0, false, init); + int[] copy = init == null ? new int[0] : Arrays.copyOf(init, init.length); + return new LocalDecl(name, FieldType.INT_ARRAY, 0, false, copy); } @Override diff --git a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java index 91a4ea7..a161a6d 100644 --- a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java +++ b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java @@ -49,7 +49,12 @@ private void registerBuiltins() { if (!el.isJsonPrimitive() || !el.getAsJsonPrimitive().isNumber()) { throw new RegistryException("Entry in 'cs_pcs' must be an integer at index " + i); } - csPcs[i] = el.getAsInt(); + try { + csPcs[i] = el.getAsJsonPrimitive().getAsBigDecimal().intValueExact(); + } catch (ArithmeticException | NumberFormatException ex) { + throw new RegistryException( + "Entry in 'cs_pcs' must be an in-range integer at index " + i, ex); + } } } else { int t0Pc = JsonHelper.getInt(json, "thread0_cs_pc", "mutual_exclusion_peterson"); @@ -59,9 +64,10 @@ private void registerBuiltins() { return (state, config) -> { PetersonState ps = (PetersonState) state; List pcs = config.programCounters(); + int limit = Math.min(csPcs.length, Math.min(pcs.size(), ps.threadCount())); int inCs = 0; - for (int i = 0; i < csPcs.length; i++) { - if (i < pcs.size() && ps.flag(i) && pcs.get(i) >= csPcs[i]) { + for (int i = 0; i < limit; i++) { + if (ps.flag(i) && pcs.get(i) >= csPcs[i]) { inCs++; if (inCs > 1) { return false; diff --git a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java index 7c9fc2b..9cd588e 100644 --- a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java +++ b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java @@ -104,6 +104,11 @@ void mutualExclusionPeterson_holds_whenBothFlagsTrueButNotBothInCS() { assertFalse(invariant.holds(after.state(), after), "the CS zone includes counters past its boundary"); } + /** + * Verifies that invalid shapes for the {@code cs_pcs} array are rejected: + * non-array parameters, arrays with fewer than 2 entries, non-numeric values, + * fractional floats, and out-of-range integers. + */ @Test void mutualExclusionPeterson_csPcs_validation() { var notArr = new com.google.gson.JsonObject(); @@ -128,8 +133,31 @@ void mutualExclusionPeterson_csPcs_validation() { notNum.add("cs_pcs", badArr); RegistryException ex3 = assertThrows(RegistryException.class, () -> registry.create(notNum)); assertTrue(ex3.getMessage().contains("must be an integer at index 1")); + + var fractional = new com.google.gson.JsonObject(); + fractional.addProperty("type", "mutual_exclusion_peterson"); + var fracArr = new com.google.gson.JsonArray(); + fracArr.add(1); + fracArr.add(1.9); + fractional.add("cs_pcs", fracArr); + RegistryException ex4 = assertThrows(RegistryException.class, () -> registry.create(fractional)); + assertTrue(ex4.getMessage().contains("must be an in-range integer at index 1")); + + var overflow = new com.google.gson.JsonObject(); + overflow.addProperty("type", "mutual_exclusion_peterson"); + var overArr = new com.google.gson.JsonArray(); + overArr.add(1); + overArr.add(new java.math.BigDecimal("-2147483649")); + overflow.add("cs_pcs", overArr); + RegistryException ex5 = assertThrows(RegistryException.class, () -> registry.create(overflow)); + assertTrue(ex5.getMessage().contains("must be an in-range integer at index 1")); } + /** + * Verifies mutual exclusion evaluation for three threads configured with {@code cs_pcs}: + * holds when 0 or 1 thread is in the critical section, and violates when two threads + * (including thread 2) or all three threads are in their critical sections simultaneously. + */ @Test void mutualExclusionPeterson_threeThreads_withCsPcs() { var json = new com.google.gson.JsonObject(); @@ -150,9 +178,9 @@ void mutualExclusionPeterson_threeThreads_withCsPcs() { Configuration cOne = Configuration.forTest(sOne, List.of(2, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); assertTrue(invariant.holds(sOne, cOne)); - // Two in CS -> violation - PetersonState sTwo = PetersonState.of(new boolean[]{true, true, false}, 0); - Configuration cTwo = Configuration.forTest(sTwo, List.of(2, 2, 1), List.of(3, 3, 3), List.of(0, 1, 2)); + // Two in CS -> violation (threads 1 and 2 in CS, ensuring thread 2 is checked) + PetersonState sTwo = PetersonState.of(new boolean[]{false, true, true}, 0); + Configuration cTwo = Configuration.forTest(sTwo, List.of(1, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); assertFalse(invariant.holds(sTwo, cTwo)); // All three in CS -> violation diff --git a/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java b/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java index 4e38129..bd2b454 100644 --- a/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java +++ b/src/test/java/dev/samhb/interleave/format/ProgramLoaderTest.java @@ -343,8 +343,11 @@ void loadMutualExclusionPeterson_twoThreads_succeeds() { assertEquals("test", program.name()); } + /** + * Verifies that a three-thread Peterson program configured with {@code cs_pcs} loads successfully + * with its invariant present, and that the loaded invariant evaluates mutual exclusion across all three threads. + */ @Test - /** Tests loadMutualExclusionPeterson_threeThreads_withCsPcs_succeeds. */ void loadMutualExclusionPeterson_threeThreads_withCsPcs_succeeds() { String json = """ { @@ -362,10 +365,21 @@ void loadMutualExclusionPeterson_threeThreads_withCsPcs_succeeds() { BenchmarkProgram program = loader.load(json); assertNotNull(program); assertEquals("test-3t", program.name()); + assertTrue(program.invariant().isPresent()); + + // Check invariant behavior on loaded program: violation when threads 1 and 2 are in CS + dev.samhb.interleave.search.Invariant inv = program.invariant().get(); + dev.samhb.interleave.core.PetersonState s = dev.samhb.interleave.core.PetersonState.of(new boolean[]{false, true, true}, 0); + dev.samhb.interleave.core.Configuration c = dev.samhb.interleave.core.Configuration.forTest( + s, List.of(0, 1, 1), List.of(1, 1, 1), List.of(0, 1, 2)); + assertFalse(inv.holds(s, c)); } + /** + * Verifies that specifying a {@code cs_pcs} array whose length differs from the thread count + * is rejected during loading with an explanatory error message. + */ @Test - /** Tests loadMutualExclusionPeterson_csPcsLengthMismatch_throwsRegistryException. */ void loadMutualExclusionPeterson_csPcsLengthMismatch_throwsRegistryException() { String json = """ { diff --git a/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java b/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java index bd3cc2e..ce192f1 100644 --- a/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java +++ b/src/test/java/dev/samhb/interleave/format/dsl/DslLocalArrayTest.java @@ -16,6 +16,7 @@ import static org.junit.jupiter.api.Assertions.assertArrayEquals; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertThrows; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -27,7 +28,10 @@ class DslLocalArrayTest { private final ProgramLoader loader = new ProgramLoader(); - /** Tests valid declaration and execution of a program with local arrays. */ + /** + * Verifies valid declaration, state loading, and end-to-end execution of a program with local arrays, + * inspecting the final state to assert that the array element was updated. + */ @Test void loadAndExecute_localArrayProgram_succeeds() { String json = """ @@ -60,10 +64,36 @@ void loadAndExecute_localArrayProgram_succeeds() { BenchmarkProgram prog = loader.load(json); assertNotNull(prog); + java.util.List visited = new java.util.ArrayList<>(); DfsExplorer explorer = new DfsExplorer(); - DfsResult result = explorer.explore(prog.program(), null, new HashingStateStore(), null); + DfsResult result = explorer.explore(prog.program(), null, new HashingStateStore(), c -> { + if (c.state() instanceof DynamicState ds) { + visited.add(ds); + } + }); assertNotNull(result); assertEquals(2, result.statesExplored()); + assertFalse(visited.isEmpty()); + DynamicState terminal = visited.getLast(); + assertArrayEquals(new int[]{10, 99, 30}, terminal.getLocalArray(0, "items")); + } + + /** Verifies that a null local-array initializer normalizes to an empty array without throwing in DynamicState. */ + @Test + void nullInitializer_normalizesToEmptyArrayAndInitializesWithoutThrowing() { + LocalDecl declNull = LocalDecl.ofArray("buf", null); + assertNotNull(declNull.arrayInit()); + assertEquals(0, declNull.arrayInit().length); + + StateDecl stateDecl = new StateDecl( + List.of(FieldDecl.ofInt("x", 0)), + List.of(declNull) + ); + DynamicState state = new DynamicState(stateDecl, 2); + assertNotNull(state.getLocalArray(0, "buf")); + assertEquals(0, state.getLocalArray(0, "buf").length); + assertNotNull(state.getLocalArray(1, "buf")); + assertEquals(0, state.getLocalArray(1, "buf").length); } /** Tests thread isolation for local arrays. */ @@ -85,7 +115,7 @@ void localArray_threadIsolation() { assertArrayEquals(new int[]{1, 2, 3}, state.getLocalArray(1, "buf")); } - /** Tests memory footprint derivation for static and dynamic local array accesses. */ + /** Verifies memory footprint derivation for static and dynamic local array accesses. */ @Test void stepFootprint_localArrayReadsAndWrites() { StateDecl decl = new StateDecl( @@ -111,7 +141,7 @@ void stepFootprint_localArrayReadsAndWrites() { assertEquals(Set.of(MemoryLocation.of("t0.buf"), MemoryLocation.of("t0.i")), stepGuard.reads()); } - /** Tests runtime out-of-bounds error handling. */ + /** Verifies runtime out-of-bounds error handling in guards and effects evaluating to ASSERTION_FAILED. */ @Test void outOfBounds_evaluatesToAssertionFailed() { StateDecl decl = new StateDecl( @@ -134,7 +164,7 @@ void outOfBounds_evaluatesToAssertionFailed() { assertEquals(StepOutcome.ASSERTION_FAILED, stepWrite.execute(state)); } - /** Tests validation error on local array without index in expression. */ + /** Verifies validation error when a local array is referenced without an index as a scalar. */ @Test void validation_localArrayWithoutIndexInExpr_throws() { String json = """ @@ -159,7 +189,7 @@ void validation_localArrayWithoutIndexInExpr_throws() { assertTrue(ex.getMessage().contains("cannot be used as scalar: use local.arr[index]")); } - /** Tests validation error on whole local array assignment. */ + /** Verifies validation error when a whole local array is assigned without an element index. */ @Test void validation_localArrayWholeAssignment_throws() { String json = """ @@ -184,7 +214,7 @@ void validation_localArrayWholeAssignment_throws() { assertTrue(ex.getMessage().contains("requires index: use local.arr[expr]")); } - /** Tests validation error on non-int assignment to local array element. */ + /** Verifies validation error when assigning a non-int value to a local array element. */ @Test void validation_nonIntAssignToLocalArray_throws() { String json = """ @@ -209,7 +239,7 @@ void validation_nonIntAssignToLocalArray_throws() { assertTrue(ex.getMessage().contains("requires int")); } - /** Tests validation error when local array is referenced in invariant. */ + /** Verifies that referencing local arrays in invariant expressions is rejected before property analysis. */ @Test void validation_localArrayInInvariant_throws() { String json = """ @@ -235,7 +265,7 @@ void validation_localArrayInInvariant_throws() { assertTrue(ex.getMessage().contains("Invariant must not reference local.*")); } - /** Tests local array init exceeding 64 elements limit. */ + /** Verifies that declaring a local array with more than 64 elements is rejected during loading. */ @Test void validation_localArrayTooLong_throws() { StringBuilder sb = new StringBuilder("["); From 630e1915ac47e2145f4378190f6facbd191eff33 Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 16:58:08 -0400 Subject: [PATCH 3/3] fix(invariant): fail-fast on thread count mismatch in mutual_exclusion_peterson Require exact match between invariant threshold count, configuration program counters, and PetersonState thread count rather than silently truncating evaluation with Math.min. Co-authored-by: Codex --- .../format/registry/InvariantRegistry.java | 8 ++++-- .../format/InvariantRegistryTest.java | 28 +++++++++++++++++++ 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java index a161a6d..f17a090 100644 --- a/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java +++ b/src/main/java/dev/samhb/interleave/format/registry/InvariantRegistry.java @@ -64,9 +64,13 @@ private void registerBuiltins() { return (state, config) -> { PetersonState ps = (PetersonState) state; List pcs = config.programCounters(); - int limit = Math.min(csPcs.length, Math.min(pcs.size(), ps.threadCount())); + if (csPcs.length != pcs.size() || csPcs.length != ps.threadCount()) { + throw new IllegalArgumentException("Thread count mismatch: invariant configured for " + + csPcs.length + " thresholds, but configuration has " + pcs.size() + + " program counters and state has " + ps.threadCount() + " threads"); + } int inCs = 0; - for (int i = 0; i < limit; i++) { + for (int i = 0; i < csPcs.length; i++) { if (ps.flag(i) && pcs.get(i) >= csPcs[i]) { inCs++; if (inCs > 1) { diff --git a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java index 9cd588e..58087a4 100644 --- a/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java +++ b/src/test/java/dev/samhb/interleave/format/InvariantRegistryTest.java @@ -189,6 +189,34 @@ void mutualExclusionPeterson_threeThreads_withCsPcs() { assertFalse(invariant.holds(sThree, cThree)); } + /** + * Verifies that evaluating mutual_exclusion_peterson throws IllegalArgumentException + * when thread counts mismatch between configured thresholds, configuration program counters, + * or PetersonState flags. + */ + @Test + void mutualExclusionPeterson_threadCountMismatch_throws() { + var json = new com.google.gson.JsonObject(); + json.addProperty("type", "mutual_exclusion_peterson"); + var arr = new com.google.gson.JsonArray(); + arr.add(2); + arr.add(2); + json.add("cs_pcs", arr); + Invariant invariant = registry.create(json); + + // Mismatch: invariant has 2 thresholds, but configuration has 3 pcs + PetersonState s2 = PetersonState.of(new boolean[]{false, false}, 0); + Configuration c3 = Configuration.forTest(s2, List.of(2, 2, 2), List.of(3, 3, 3), List.of(0, 1, 2)); + IllegalArgumentException ex1 = assertThrows(IllegalArgumentException.class, () -> invariant.holds(s2, c3)); + assertTrue(ex1.getMessage().contains("Thread count mismatch")); + + // Mismatch: invariant has 2 thresholds, pcs has 2, but state has 3 threads + PetersonState s3 = PetersonState.of(new boolean[]{false, false, false}, 0); + Configuration c2 = Configuration.forTest(s3, List.of(2, 2), List.of(3, 3), List.of(0, 1)); + IllegalArgumentException ex2 = assertThrows(IllegalArgumentException.class, () -> invariant.holds(s3, c2)); + assertTrue(ex2.getMessage().contains("Thread count mismatch")); + } + @Test void counterEquals_holds_whenNotTerminated() {