Progress64 benchmarks

benchmarks/progress64/README.md

@@ -0,0 +1,21 @@
+# How to generate LLVM files with Inline Asm with Progress64
+
+You need to clone [ARM-software/progress64](https://github.com/ARM-software/progress64).
+
+In this case you have to generate the clients to leverage the API on your own.
+
+Then, follow this pattern :
+```
+clang <Includes> <custom flags> -S -emit-llvm <file_path.c>
+```
+The Includes should contain :
+1. path to progress64/include
+2. path to progress64/src
+
+The Custom flags should be set up accordingly to your client. In some cases, if you do not get inline asm, try to add :
+1. ```-U__ARM_FEATURE_ATOMICS``` to force the compiler to avoid including the builtins
+
+A valid example would therefore be, from root of progress64 :
+```
+clang -I <path_to_progress64>/include -I <path_to_progress64>/src -S -emit-llvm benchmarks/progress64/rwlock.c
+```

benchmarks/progress64/rwlock.c

@@ -0,0 +1,34 @@
+#include <pthread.h>
+#include <assert.h>
+#include "p64_rwlock.c"
+
+#define NTHREADS 3
+
+
+void *run(void *arg) {
+    p64_rwlock_acquire_wr(&lock);
+    x++;
+    y++;
+    p64_rwlock_release_wr(&lock);
+    return NULL;
+}
+
+int main() {
+    pthread_t threads[NTHREADS];
+    p64_rwlock_init(&lock);
+
+    for (int i = 0; i < NTHREADS; i++) {
+        if (pthread_create(&threads[i], NULL, run, (void *)(long)i) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+
+    for (int i = 0; i < NTHREADS; i++) {
+        if (pthread_join(threads[i], NULL) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+
+    assert(x == NTHREADS && y == NTHREADS);
+    return 0;
+}

benchmarks/progress64/seqlock.c

@@ -0,0 +1,57 @@
+#include <assert.h>
+#include <pthread.h>
+#include "p64_rwsync.c"
+
+typedef struct {
+    int x;
+    int y;
+} shared_data_t;
+
+p64_rwsync_t sync;
+shared_data_t data;
+
+void *writer(void *arg) {
+    p64_rwsync_acquire_wr(&sync);
+    data.x++;
+    data.y++;
+    p64_rwsync_release_wr(&sync);
+    return NULL;
+}
+
+void *reader(void *arg) {
+    shared_data_t local;
+    p64_rwsync_read(&sync, &local, &data, sizeof(local));
+    return NULL;
+}
+
+int main(void) {
+    pthread_t writers[2], readers[2];
+    p64_rwsync_init(&sync);
+    data.x = 0;
+    data.y = 0;
+
+    for (int i = 0; i < 2; i++) {
+        if (pthread_create(&writers[i], NULL, writer, NULL) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+    for (int i = 0; i < 2; i++) {
+        if (pthread_create(&readers[i], NULL, reader, NULL) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+
+    for (int i = 0; i < 2; i++) {
+        if (pthread_join(writers[i], NULL) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+
+    for (int i = 0; i < 2; i++) {
+        if (pthread_join(readers[i], NULL) != 0) {
+            exit(EXIT_FAILURE);
+        }
+    }
+    assert(data.x == 2 && data.y == 2);
+    return 0;
+}

dartagnan/src/test/java/com/dat3m/dartagnan/asm/armv8/progress64/AsmProgress64Armv8Test.java

@@ -0,0 +1,89 @@
+package com.dat3m.dartagnan.asm.armv8.progress64;
+
+import java.io.File;
+import java.io.IOException;
+import java.util.Arrays;
+import java.util.EnumSet;
+
+import static org.junit.Assert.assertEquals;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+import org.sosy_lab.common.ShutdownManager;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.BasicLogManager;
+import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.api.SolverContext;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC;
+import static com.dat3m.dartagnan.configuration.Property.TERMINATION;
+import com.dat3m.dartagnan.encoding.ProverWithTracker;
+import com.dat3m.dartagnan.parsers.cat.ParserCat;
+import com.dat3m.dartagnan.parsers.program.ProgramParser;
+import com.dat3m.dartagnan.program.Program;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
+import com.dat3m.dartagnan.utils.Result;
+import static com.dat3m.dartagnan.utils.Result.PASS;
+import com.dat3m.dartagnan.verification.VerificationTask;
+import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
+import com.dat3m.dartagnan.wmm.Wmm;
+
+@RunWith(Parameterized.class)
+public class AsmProgress64Armv8Test {
+
+    private final String modelPath = getRootPath("cat/aarch64.cat");
+    private final String programPath;
+    private final int bound;
+    private final Result expected;
+
+    public AsmProgress64Armv8Test (String file, int bound, Result expected) {
+        this.programPath = getTestResourcePath("asm/armv8/progress64/" + file + ".ll");
+        this.bound = bound;
+        this.expected = expected;
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}")
+    public static Iterable<Object[]> data() throws IOException {
+        return Arrays.asList(new Object[][]{
+            {"rwlock", 1, PASS},
+            {"seqlock", 3, PASS},
+        });
+    }
+
+    @Test
+    public void testAllSolvers() throws Exception {
+        try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
+            assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
+        }
+        try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) {
+            assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
+        }
+    }
+
+    private SolverContext mkCtx() throws InvalidConfigurationException {
+        Configuration cfg = Configuration.builder().build();
+        return SolverContextFactory.createSolverContext(
+                cfg,
+                BasicLogManager.create(cfg),
+                ShutdownManager.create().getNotifier(),
+                SolverContextFactory.Solvers.YICES2);
+    }
+
+    private ProverWithTracker mkProver(SolverContext ctx) {
+        return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS);
+    }
+
+    private VerificationTask mkTask() throws Exception {
+        VerificationTask.VerificationTaskBuilder builder = VerificationTask.builder()
+                .withConfig(Configuration.builder().build())
+                .withBound(bound)
+                .withTarget(Arch.ARM8);
+        Program program = new ProgramParser().parse(new File(programPath));
+        Wmm mcm = new ParserCat().parse(new File(modelPath));
+        return builder.build(program, mcm, EnumSet.of(TERMINATION, PROGRAM_SPEC));
+    }
+}