| // 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 |
| // non-concurrent writes. In other words, write operations never overlap each |
| // other, and all write operations have a well-defined order. |
| // |
| // A system in which all write operations came from a single thread would |
| // satisfy these requirements, as would one where some external mechanism |
| // guarantees that the writes are ordered and non-overlapping. The sequence |
| // number in this system is used only as a transaction failure detector for |
| // readers, not to guarantee the writer requirements. |
| // |
| // 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 not execute concurrently, and all write transactions must have |
| // a well defined order relative to each other. |
| // ++ 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. |
| // |
| |
| constexpr uint32_t kPayloadWords = 3; |
| constexpr uint32_t kTotalWrites = 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) { |
| } |
| |
| // 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, uint32_t start_val) { |
| // Increment the sequence number with relaxed semantics |
| s.seq.fetch_add(1u, std::memory_order_relaxed); |
| |
| // Store the payloads, each with release semantics. |
| for (size_t i = 0; i < s.payload.size(); ++i) { |
| s.payload[i].store(start_val + i, 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, writer; |
| |
| thrd_create( |
| &reader, |
| [](void* ctx) { |
| State& s = *reinterpret_cast<State*>(ctx); |
| Read(s); |
| }, |
| &s); |
| |
| thrd_create( |
| &writer, |
| [](void* ctx) { |
| State& s = *reinterpret_cast<State*>(ctx); |
| for (uint32_t i = 1; i <= kTotalWrites; ++i) { |
| Write(s, kPayloadWords * i); |
| } |
| }, |
| &s); |
| |
| thrd_join(reader); |
| thrd_join(writer); |
| |
| return 0; |
| } |