Mixed-size accesses

benchmarks/mixed/lockref1.c

@@ -0,0 +1,103 @@
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+
+
+#ifndef NTHREADS
+#define NTHREADS 3
+#endif
+
+// ==========================================
+//                   Spinlock
+// ==========================================
+
+struct spinlock_s {
+        _Atomic(int32_t) lock;
+};
+typedef struct spinlock_s spinlock_t;
+
+void await_for_lock(struct spinlock_s *l)
+{
+    while (atomic_load_explicit(&l->lock, memory_order_relaxed) != 0);
+    return;
+}
+
+int try_get_lock(struct spinlock_s *l)
+{
+    int val = 0;
+    return atomic_compare_exchange_strong_explicit(&l->lock, &val, 1, memory_order_acquire, memory_order_acquire);
+}
+
+void spin_lock(struct spinlock_s *l)
+{
+    do {
+        await_for_lock(l);
+    } while(!try_get_lock(l));
+    return;
+}
+
+void spin_unlock(struct spinlock_s *l)
+{
+    atomic_store_explicit(&l->lock, 0, memory_order_release);
+}
+
+// ==========================================
+//                   Lockref
+// ==========================================
+
+typedef struct {
+    union {
+        struct {
+            atomic_int lock;
+            int count;
+        };
+        atomic_long lock_count;
+    };
+} lockref_t;
+
+void lockref_get(lockref_t *lockref) {
+    long old_val = atomic_load_explicit(&lockref->lock_count, memory_order_relaxed);
+
+    while (((lockref_t *)&old_val)->lock == 0) {
+        long new_val = old_val;
+        ((lockref_t *)&new_val)->count++;
+        if (atomic_compare_exchange_strong_explicit(
+                &lockref->lock_count, &old_val, new_val,
+                memory_order_relaxed, memory_order_relaxed)) {
+            return;
+        }
+    }
+
+    spin_lock(&lockref->lock);
+    lockref->count++;
+    spin_unlock(&lockref->lock);
+}
+
+// ==========================================
+//                     Main
+// ==========================================
+
+lockref_t my_lockref;
+
+void *thread_n(void *unsued) {
+
+    lockref_get(&my_lockref);
+
+    return NULL;
+}
+
+int main() {
+
+    pthread_t t[NTHREADS];
+
+    atomic_store(&my_lockref.lock_count, 0);
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_create(&t[i], 0, thread_n, (void *)(size_t)i);
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_join(t[i], 0);
+
+    assert(my_lockref.count == NTHREADS);
+    return 0;
+}

benchmarks/mixed/lockref2.c

@@ -0,0 +1,101 @@
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+
+#ifndef NTHREADS
+#define NTHREADS 3
+#endif
+
+// ==========================================
+//                   Spinlock
+// ==========================================
+
+struct spinlock_s {
+        _Atomic(int32_t) lock;
+};
+typedef struct spinlock_s spinlock_t;
+
+void await_for_lock(struct spinlock_s *l)
+{
+    while (atomic_load_explicit(&l->lock, memory_order_relaxed) != 0);
+    return;
+}
+
+int try_get_lock(struct spinlock_s *l)
+{
+    int val = 0;
+    return atomic_compare_exchange_strong_explicit(&l->lock, &val, 1, memory_order_acquire, memory_order_acquire);
+}
+
+void spin_lock(struct spinlock_s *l)
+{
+    do {
+        await_for_lock(l);
+    } while(!try_get_lock(l));
+    return;
+}
+
+void spin_unlock(struct spinlock_s *l)
+{
+    atomic_store_explicit(&l->lock, 0, memory_order_release);
+}
+
+// ==========================================
+//                   Lockref
+// ==========================================
+
+struct lockref {
+    union {
+        _Atomic(int64_t) lock_count;
+        struct {
+            spinlock_t lock;
+            _Atomic(int32_t) count;
+        };
+    };
+};
+
+void lockref_get(struct lockref *lockref) {
+    struct lockref old;
+
+    old.lock_count = atomic_load_explicit(&lockref->lock_count, memory_order_relaxed);
+    while (old.lock.lock == 0) {
+        struct lockref new = old;
+        new.count++;
+        if (atomic_compare_exchange_strong_explicit(&lockref->lock_count, (int64_t *) &old.lock_count, new.lock_count, memory_order_relaxed, memory_order_relaxed)) {
+            return;
+        }
+    }
+
+    spin_lock(&lockref->lock);
+    lockref->count++;
+    spin_unlock(&lockref->lock);
+}
+
+// ==========================================
+//                     Main
+// ==========================================
+
+struct lockref my_lockref;
+
+void *thread_n(void *unsued) {
+
+    lockref_get(&my_lockref);
+
+    return NULL;
+}
+
+int main() {
+
+    pthread_t t[NTHREADS];
+
+    atomic_store(&my_lockref.lock_count, 0);
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_create(&t[i], 0, thread_n, (void *)(size_t)i);
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_join(t[i], 0);
+
+    assert(my_lockref.count == NTHREADS);
+    return 0;
+}

cat/aarch64.cat

@@ -1,12 +1,18 @@
 (*
- * The ARMv8 Application Level Memory Model.
+ * The Armv8 Application Level Memory Model.
  *
- * See section B2.3 of the ARMv8 ARM:
+ * This is a machine-readable, executable and formal artefact, which aims to be
+ * the latest stable version of the Armv8 memory model.
+ * If you have comments on the content of this file, please send an email to
+ * [email protected], referring to version number:
+ * 814a6fc1610ec1a24f2cbd178e171966375626ac
+ * For a textual version of the model, see section B2.3 of the Armv8 ARM:
  *   https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile
  *
  * Author: Will Deacon <[email protected]>
+ * Author: Jade Alglave <[email protected]>
  *
- * Copyright (C) 2016, ARM Ltd.
+ * Copyright (C) 2016-2020, Arm Ltd.
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -44,10 +50,10 @@
  * location and then consequently defines the fr relation using co and
  * rf.
  *)
-include "cos.cat"
+include "coscat.cat"
 
 (*
- * Include aarch64fences.cat so that barriers show up in generated diagrams.
+ * Include aarch64fences.cat to define barriers.
  *)
 include "aarch64fences.cat"
 
@@ -79,32 +85,40 @@ flag ~empty (dmb.full | dmb.ld | dmb.st) \
 (* Coherence-after *)
 let ca = fr | co
 
+(* Local read successor *)
+let lrs = [W]; (po-loc \ (po-loc;[W];po-loc)) ; [R]
+
+(* Local write successor *)
+let lws = po-loc; [W]
+
 (* Observed-by *)
 let obs = rfe | fre | coe
 
 (* Dependency-ordered-before *)
-let dob = addr | data
+let dob = (addr | data)
 	| ctrl; [W]
 	| (ctrl | (addr; po)); [ISB]; po; [R]
 	| addr; po; [W]
-	| (ctrl | data); coi
-	| (addr | data); rfi
+	| (addr | data); lrs
 
 (* Atomic-ordered-before *)
 let aob = rmw
-	| [range(rmw)]; rfi; [A | Q]
+	| [range(rmw)]; lrs; [A | Q]
 
 (* Barrier-ordered-before *)
 let bob = po; [dmb.full]; po
+	| po; ([A];amo;[L]); po
 	| [L]; po; [A]
 	| [R]; po; [dmb.ld]; po
 	| [A | Q]; po
 	| [W]; po; [dmb.st]; po; [W]
 	| po; [L]
-	| po; [L]; coi
+
+(* Locally-ordered-before *)
+let lob = lws; si | dob | aob | bob
 
 (* Ordered-before *)
-let ob = obs | dob | aob | bob
+let ob = obs; si | lob
 
 (* Internal visibility requirement *)
 acyclic po-loc | ca | rf as internal

cat/stdlib.cat

@@ -1,6 +1,7 @@
 let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W]
 
 let po-loc = po & loc
+let rmw = amo | lxsx
 
 let rfe = rf & ext
 let coe = co & ext