Add integration test for Condition.await and Condition.signal based on SCTBench example.

.github/workflows/main.yml

@@ -0,0 +1,29 @@
+name: CI
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+  workflow_dispatch:
+jobs:
+  build-and-test:
+    runs-on: ubuntu-latest
+    permissions: 
+      contents: read
+      packages: read 
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+          cache: 'gradle'
+      - name: Build sfuzz (no tests)
+        run: ./gradlew build -x test
+      - name: Instrument JDK
+        run: ./gradlew jlink
+      - name: Build shadow JAR
+        run: ./gradlew shadowJar
+      - name: Test sfuzz
+        run: ./gradlew test
+

examples/build.gradle.kts

@@ -58,7 +58,7 @@ tasks.register<JavaExec>("runArithmeticProgSfuzz") {
     classpath = sourceSets["main"].runtimeClasspath
     executable("${jdk.layout.buildDirectory.get().asFile}/java-inst/bin/java")
     mainClass.set("cmu.pasta.sfuzz.core.MainKt")
-    args = listOf("example.ArithmeticProgBad", "-o", "${layout.buildDirectory.get().asFile}/report", "--scheduler", "fifo")
+    args = listOf("example.ArithmeticProgBad", "main", "-o", "${layout.buildDirectory.get().asFile}/report", "--scheduler", "fifo")
     jvmArgs("-agentpath:${agentPath}")
     jvmArgs("-javaagent:${instrumentation.layout.buildDirectory.get().asFile}/libs/${instrumentation.name}-${instrumentation.version}-all.jar")
     doFirst {

integration-tests/src/test/java/cmu/pasta/sfuzz/it/core/ConditionTest.java

@@ -0,0 +1,11 @@
+package cmu.pasta.sfuzz.it.core;
+
+import cmu.pasta.sfuzz.it.IntegrationTestRunner;
+import org.junit.jupiter.api.Test;
+
+public class ConditionTest extends IntegrationTestRunner {
+    @Test
+    public void testInterleaving1() {
+        runTest("main");
+    }
+}

integration-tests/src/test/java/example/ConditionTest.java

@@ -0,0 +1,96 @@
+package example;
+
+import java.util.concurrent.locks.Condition;
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+import cmu.pasta.sfuzz.core.GlobalContext;
+
+public class ConditionTest {
+
+    private static int num;
+    private static long total;
+    private static boolean flag;
+
+    private static Lock m = new ReentrantLock();
+    private static int N = 3;
+    private static Condition empty = m.newCondition();
+    private static Condition full = m.newCondition();
+
+    private void log (String format, Object... args) {
+        GlobalContext.INSTANCE.log(format, args);
+    }
+
+    public static void main(String[] args) {
+        ConditionTest t = new ConditionTest();
+        t.testConditionAwait();
+    }
+
+    public void testConditionAwait() {
+
+        Thread producer = new Thread (() -> {
+            int i = 0;
+            while (i < N) {
+                m.lock();
+                log("Acquired lock.\n");
+
+                try {
+                    while (num > 0) {
+                        log("Beginning empty await.\n");
+                        empty.await();
+                        log("Returned from empty await.\n");
+                    }
+                    num++;
+                    full.signal();
+                    log("Sent full signal.\n");
+
+                } catch (InterruptedException e) {
+                } finally {
+                    m.unlock();
+                    log("Released lock.\n");
+                }
+
+
+                i++;
+          }
+        });
+
+        Thread consumer = new Thread (() -> {
+            int j = 0;
+            while (j < N) {
+                m.lock();
+                log("Acquired lock.\n");
+                try {
+                    while (num == 0) {
+                        log("Beginning full await.\n");
+                        full.await();
+                        log("Returned from full await.\n");
+                    }
+                    total = total + j;
+                    num--;
+                    empty.signal();
+                    log("Sent empty signal.\n");
+                } catch (InterruptedException e) {
+                } finally {
+                    m.unlock();
+                    log("Released lock.\n");
+                }
+
+                j++;
+            }
+            total = total + j;
+            flag = true;
+        });
+
+        producer.start();
+        consumer.start();
+
+        try {
+            producer.join();
+            consumer.join();
+        } catch (InterruptedException e) {
+            throw new RuntimeException(e);
+        }
+
+        assert total == ((N * (N + 1)) / 2);
+    }
+}

integration-tests/src/test/resources/expected/ConditionTest_Fifo.txt

@@ -0,0 +1,23 @@
+[1]: Acquired lock.
+[1]: Sent full signal.
+[1]: Released lock.
+[1]: Acquired lock.
+[1]: Beginning empty await.
+[2]: Acquired lock.
+[2]: Sent empty signal.
+[2]: Released lock.
+[1]: Returned from empty await.
+[1]: Sent full signal.
+[1]: Released lock.
+[1]: Acquired lock.
+[1]: Beginning empty await.
+[2]: Acquired lock.
+[2]: Sent empty signal.
+[2]: Released lock.
+[1]: Returned from empty await.
+[1]: Sent full signal.
+[1]: Released lock.
+[2]: Acquired lock.
+[2]: Sent empty signal.
+[2]: Released lock.
+

integration-tests/src/test/resources/schedules/ConditionTest_Fifo.json

@@ -0,0 +1,110 @@
+{
+    "choices": [
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 3
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 3
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 2,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 2,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 2,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 1,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 2
+        },
+        {
+            "selected": 0,
+            "threadId": 2,
+            "enabled": 1
+        },
+        {
+            "selected": 0,
+            "threadId": 0,
+            "enabled": 1
+        }
+    ],
+    "fullSchedule": true
+}