| // Copyright 2023 The Fuchsia Authors. All rights reserved. |
| // Use of this source code is governed by a BSD-style license that can be |
| // found in the LICENSE file. |
| |
| #include <stdint.h> |
| #include <stdio.h> |
| #include <threads.h> |
| |
| #include <array> |
| #include <atomic> |
| |
| #include "librace.h" |
| #include "model-assert.h" |
| |
| // |
| // Requirements: |
| // |
| // Design A SeqLock which is intended to allow concurrent reads, and write |
| // transactions from different threads running concurrently. The sequence |
| // number itself serves both as the transaction failure detector for readers, as |
| // well as the spinlock-style exclusive lock for writers. |
| // |
| // The SeqLock implementation described in this example must tolerate the |
| // following thread behaviors, and obey the following rules. |
| // |
| // ++ Readers are allowed to execute concurrently with writers |
| // ++ Writer may attempt to execute concurrently (from multiple threads), but |
| // the SeqLock implementation must not allow them to modify the payload at |
| // the same time. |
| // ++ Writers may read the payload contents during a transaction, in addition to |
| // writing them. |
| // ++ Payload AcqRel semantics are used in this example, instead of fences. |
| // |
| // The outline of read and write transactions look like the following. |
| // |
| // :: Read Transaction :: |
| // 1) while ((before = Seq) & 0x1) {}; // Acquire semantics |
| // 2) ReadPayload() // Acquire semantics for all members |
| // 4) after = Seq; // Relaxed semantics |
| // 5) if (before != after) goto 1; |
| // |
| // :: Write Transaction :: |
| // 1) while ((before = Seq) & 0x1) {}; // Relaxed semantics |
| // 2) if (!CMPX(Seq, before + 1)) goto 1; // Acquire semantics |
| // 2) WritePayload() // Release semantics for all members |
| // 3) Seq += 1; // Release semantics |
| // |
| constexpr uint32_t kPayloadWords = 2; |
| constexpr uint32_t kTotalWriters = 2; |
| |
| struct State { |
| std::atomic<uint64_t> seq; |
| std::array<std::atomic<uint32_t>, kPayloadWords> payload; |
| }; |
| |
| static void Read(State& s) { |
| uint64_t before, after; |
| std::array<uint32_t, kPayloadWords> vals; |
| |
| do { |
| // spin until we see an even sequence number using acq loads. |
| while ((before = s.seq.load(std::memory_order_acquire)) & 1u) { |
| thrd_yield(); |
| } |
| |
| // Load all payloads with acquire. |
| for (uint32_t i = 0; i < vals.size(); ++i) { |
| vals[i] = s.payload[i].load(std::memory_order_acquire); |
| } |
| |
| // Load the sequence number again, this time relaxed |
| after = s.seq.load(std::memory_order_relaxed); |
| } while (before != after); |
| |
| MODEL_ASSERT((vals[0] % kPayloadWords) == 0); |
| for (uint32_t i = 1; i < vals.size(); ++i) { |
| MODEL_ASSERT((vals[i - 1] + 1) == vals[i]); |
| } |
| } |
| |
| static void Write(State& s) { |
| // Spin until we observe an even sequence number using relaxed semantics. |
| // Then attempt to increment that even number using acquire semantics. |
| uint64_t seq; |
| do { |
| while ((seq = s.seq.load(std::memory_order_relaxed)) & 1u) { |
| thrd_yield(); |
| } |
| } while (!s.seq.compare_exchange_strong(seq, seq + 1, std::memory_order_acquire, |
| std::memory_order_relaxed)); |
| |
| // Store the payloads, each with release semantics. |
| for (size_t i = 0; i < s.payload.size(); ++i) { |
| s.payload[i].fetch_add(kPayloadWords, std::memory_order_release); |
| } |
| |
| // Increment the sequence number again, this time with release. |
| s.seq.fetch_add(1u, std::memory_order_release); |
| } |
| |
| extern "C" int user_main(int argc, char** argv) { |
| State s; |
| |
| printf("Seq = %p\n", &s.seq); |
| s.seq.store(0u); |
| for (uint32_t i = 0; i < s.payload.size(); ++i) { |
| printf("p[%i] = %p\n", i, &s.payload[i]); |
| s.payload[i].store(i); |
| } |
| |
| thrd_t reader; |
| std::array<thrd_t, kTotalWriters> writers; |
| |
| thrd_create( |
| &reader, [](void* ctx) { Read(*reinterpret_cast<State*>(ctx)); }, &s); |
| |
| for (auto& writer : writers) { |
| thrd_create( |
| &writer, [](void* ctx) { Write(*reinterpret_cast<State*>(ctx)); }, &s); |
| } |
| |
| thrd_join(reader); |
| for (auto& writer : writers) { |
| thrd_join(writer); |
| } |
| |
| return 0; |
| } |