// 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 exclusive
// writes.  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 not* read the payload during the transaction.  IOW,
//    they may only write new values to the payload, which do not
//    depend on the old values.
// ++ Payload AcqRel semantics are to be used in this example, instead
//    of fences.
//
// The Hypothesis:
//
// A minimal implementation of a SeqLock where all writes came from a
// single thread would look something like this:
//
// :: Read Transaction ::
// 1) while ((before = Seq) & 0x1) {};  // Acquire semantics
// 2) Read Payload;                     // Acquire semantics for all members
// 3) after = Seq;                      // Relaxed semantics
// 4) if (before != after) repeat;
//
// :: Write Transaction ::
// 1) Seq += 1;      // Relaxed semantics
// 2) Write Payload; // Release semantics for all members
// 3) Seq += 1;      // Release semantics
//
// If we wish to extend this to allow writes to come in from multiple
// threads, we need to make sure that two writers are not allowed to
// modify the payload at the same time.  So, we use the "odd sequence
// number implies write-in-flight" property of our sequence number to
// cause writers to wait in line.  The new sequence is now:
//
// :: Write Transaction ::
// 1) while ((observed = Seq) & 0x1) {};         // Relaxed semantics
// 2) if (!CMPX(observed, observed +1)) goto 1;  // Relaxed semantics
// 3) Write Payload;                             // Release semantics for all members
// 4) Seq += 1;                                  // Release semantics
//
// Note that there are no acquire semantics on either step #1 or step #2.  There
// are no loads of any of the payload values in step #3, so there is nothing in
// step #3 which would be need to be prevented from moving up before steps #1,2.
// Therefore, a load-acquire operation at that point in the sequence would serve
// no purpose, right?
//
// Turns out, the answer is "No, this is not fine".
//
// The Failure:
//
// The CDS-checker model (below) finds the problem with this idea.  We model a
// system with one reader (R1), and two writers (W1 and W2), all executing
// concurrently.  After a successful read, the reader must have observed one of
// the following:
//
// 1) The initial state of the payload.
// 2) The state of the payload as written by W1.
// 3) The state of the payload as written by W2.
//
// Any mixing of the payload would be a failure, and indeed, this does fail.
// Here is one example from the checker.  The addresses of the accesses have
// been "symbolized" for ease of reading, and unrelated accesses (those used
// when launching threads) have been removed.  Finally, the full sequence is
// presented in execution order, and then again grouped by thread.
//
// 1) The initial state of the payload is P = (0, 1)
// 2) W1 writes P = (2, 3)
// 3) W2 writes P = (4, 5)
//
// ------------------------------------------------------------------------------------
// #    t    Action type     MO       Location         Value               Rf  CV
// ------------------------------------------------------------------------------------
// 2    1    atomic write    seq_cst  Seq              0                       ( 0,  2)
// 3    1    atomic write    seq_cst  p[0]             0                       ( 0,  3)
// 4    1    atomic write    seq_cst  p[1]             0x1                     ( 0,  4)
// 7    2    atomic read     acquire  Seq              0                   2   ( 0,  5,  7)
// 10   2    atomic read     acquire  p[0]             0                   3   ( 0,  5, 10)
// 11   3    atomic read     relaxed  Seq              0                   2   ( 0,  8,  0, 11)
// 14   2    atomic read     acquire  p[1]             0x1                 4   ( 0,  5, 14)
// 15   3    atomic rmw      relaxed  Seq              0                   2   ( 0,  8,  0, 15)
// 16   4    atomic read     relaxed  Seq              0                   2   ( 0, 12,  0,  0, 16)
// 17   2    atomic read     relaxed  Seq              0x1                 15  ( 0,  5, 17)
// 18   3    atomic write    release  p[0]             0x2                     ( 0,  8,  0, 18)
// 19   4    atomic read     relaxed  Seq              0x1                 15  ( 0, 12,  0,  0, 19)
// 20   2    atomic read     acquire  Seq              0x1                 15  ( 0,  5, 20)
// 21   3    atomic write    release  p[1]             0x3                     ( 0,  8,  0, 21)
// 22   4    atomic read     relaxed  Seq              0x1                 15  ( 0, 12,  0,  0, 22)
// 24   3    atomic rmw      release  Seq              0x1                 15  ( 0,  8,  0, 24)
// 26   2    atomic read     acquire  Seq              0x2                 24  ( 0,  8, 26, 24)
// 28   4    atomic read     relaxed  Seq              0x2                 24  ( 0, 12,  0,  0, 28)
// 29   2    atomic read     acquire  p[0]             0x2                 18  ( 0,  8, 29, 24)
// 30   4    atomic rmw      relaxed  Seq              0x2                 24  ( 0, 12,  0,  0, 30)
// 31   2    atomic read     acquire  p[1]             0x3                 21  ( 0,  8, 31, 24)
// 32   4    atomic write    release  p[0]             0x4                     ( 0, 12,  0,  0, 32)
// 33   2    atomic read     relaxed  Seq              0x3                 30  ( 0,  8, 33, 24)
// 34   4    atomic write    release  p[1]             0x5                     ( 0, 12,  0,  0, 34)
// 35   2    atomic read     acquire  Seq              0x3                 30  ( 0,  8, 35, 24)
// 36   4    atomic rmw      release  Seq              0x3                 30  ( 0, 12,  0,  0, 36)
// 39   2    atomic read     acquire  Seq              0x4                 36  ( 0, 12, 39, 24, 36)
// 40   2    atomic read     acquire  p[0]             0x2                 18  ( 0, 12, 40, 24, 36)
// 41   2    atomic read     acquire  p[1]             0x5                 34  ( 0, 12, 41, 24, 36)
// 42   2    atomic read     relaxed  Seq              0x4                 36  ( 0, 12, 42, 24, 36)
//
// -------------------------- The sequence seen by W1 --------------------------
//
// W1 sees no contention at all.  It grabs the "lock" and writes (2, 3) to the
// payload, then exits.
//
// 11   3    atomic read     relaxed  Seq              0                   2   ( 0,  8,  0, 11)
// 15   3    atomic rmw      relaxed  Seq              0                   2   ( 0,  8,  0, 15)
// 18   3    atomic write    release  p[0]             0x2                     ( 0,  8,  0, 18)
// 21   3    atomic write    release  p[1]             0x3                     ( 0,  8,  0, 21)
// 24   3    atomic rmw      release  Seq              0x1                 15  ( 0,  8,  0, 24)
//
// -------------------------- The sequence seen by W2 --------------------------
//
// W2 starts by reading Seq and seeing an even number.  However, we see it immediately
// read Seq again (this time observing an odd number), implying that the relaxed
// read during the strong CMPX saw a different value from what was expected, and
// therefore failed.  W2 now spins on Seq, waiting for it to become even again.
//
// 16   4    atomic read     relaxed  Seq              0                   2   ( 0, 12,  0,  0, 16)
// 19   4    atomic read     relaxed  Seq              0x1                 15  ( 0, 12,  0,  0, 19)
// 22   4    atomic read     relaxed  Seq              0x1                 15  ( 0, 12,  0,  0, 22)
//
// We see the sequence number go back to even, and this time we successfully
// increment it, write out payload, and drop the lock.
//
// 28   4    atomic read     relaxed  Seq              0x2                 24  ( 0, 12,  0,  0, 28)
// 30   4    atomic rmw      relaxed  Seq              0x2                 24  ( 0, 12,  0,  0, 30)
// 32   4    atomic write    release  p[0]             0x4                     ( 0, 12,  0,  0, 32)
// 34   4    atomic write    release  p[1]             0x5                     ( 0, 12,  0,  0, 34)
// 36   4    atomic rmw      release  Seq              0x3                 30  ( 0, 12,  0,  0, 36)
//
// -------------------------- The sequence seen by R1 --------------------------
//
// R1 starts a read sequence, and manages to observe the initial state of (0,1),
// but when it reads the sequence number the second time, it sees that the
// counter has been bumped, and it needs to try again.
//
// 7    2    atomic read     acquire  Seq              0                   2   ( 0,  5,  7)
// 10   2    atomic read     acquire  p[0]             0                   3   ( 0,  5, 10)
// 14   2    atomic read     acquire  p[1]             0x1                 4   ( 0,  5, 14)
// 17   2    atomic read     relaxed  Seq              0x1                 15  ( 0,  5, 17)
//
// So, R1 goes back to waiting for Seq to become even again.  Once it does, R1
// successfully observes (2,3), the state written by W1.  Once again, however,
// it sees the sequence number advance, and so it has to retry.
//
// 20   2    atomic read     acquire  Seq              0x1                 15  ( 0,  5, 20)
// 26   2    atomic read     acquire  Seq              0x2                 24  ( 0,  8, 26, 24)
// 29   2    atomic read     acquire  p[0]             0x2                 18  ( 0,  8, 29, 24)
// 31   2    atomic read     acquire  p[1]             0x3                 21  ( 0,  8, 31, 24)
// 33   2    atomic read     relaxed  Seq              0x3                 30  ( 0,  8, 33, 24)
//
// Back to waiting for an even sequence number.  When we finally see one, we see
// the final sequence number written by W2 (0x4) and proceed to read our
// payload.  When we get to the end, we see the sequence number is still 0x4, so
// we declare victory.
//
// 35   2    atomic read     acquire  Seq              0x3                 30  ( 0,  8, 35, 24)
// 39   2    atomic read     acquire  Seq              0x4                 36  ( 0, 12, 39, 24, 36)
// 40   2    atomic read     acquire  p[0]             0x2                 18  ( 0, 12, 40, 24, 36)
// 41   2    atomic read     acquire  p[1]             0x5                 34  ( 0, 12, 41, 24, 36)
// 42   2    atomic read     relaxed  Seq              0x4                 36  ( 0, 12, 42, 24, 36)
//
// Unfortunately, the payload we read is (2, 5).  We saw p[0] as written by W1,
// and p[1] as written by W2.  This "should" be impossible given the following
// argument:
//
// 1) The read of Seq at #39 synchronized-with the write of Seq at #36.
// 2) The subsequent loads #40-42 must therefore happen-after the write at #36.
// 3) The W2 payload stores #32,34 cannot move past the store at #36.
// 4) Therefore the payload loads #40,41 must have happened-after the stores
//    #32,34.
//
// So how did load #40 manage to see store #18?  The clock vector tells the
// tale.  Load #39 did synchronize-with store #36 in W2, so all of the
// subsequent loads did happen after W2 completed.  But, it also synchronized
// with store #18 from W1, and the loads also happened after W1 completed.
//
// The key point:
//
// The issue here is that W1 and W2 have no ordering relationship.  While R1
// happened-after both W1 and W2, W1 did not happen-after W2, or vice-versa;
// they have no defined order.  Therefore, loads done in R1 can see the state
// left by W1 after store #24 OR they can see the state left by W2 after store
// #36.  In this case, that is what happens.  p[0] comes from the W1 state, and
// p[1] comes from the W2 state.
//
// The fix:
//
// The fix here is to add acquire semantics to the initial load of Seq done
// during the write sequence.  This forces the start of every write transaction
// to synchronize with the end of the previous write transaction.  Now, all of
// the write transactions have a defined order, so when the read sequences
// initial Seq load synchronizes-with at the end of a write transaction, it can
// only see states after that write transaction, never any earlier states.
//

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 load-acquires.
    while ((before = s.seq.load(std::memory_order_acquire)) & 1u) {
      thrd_yield();
    }

    // Load all payloads with acquire semantics.
    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) {
  // Spin until we can increment the sequence number from even to odd, using
  // only relaxed 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_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;
  struct WriterState {
    State* state;
    thrd_t thread;
    uint32_t id;
  };

  std::array<WriterState, kTotalWriters> writers;
  for (uint32_t i = 0; i < writers.size(); ++i) {
    writers[i].state = &s;
    writers[i].id = i + 1;
  }

  thrd_create(
      &reader,
      [](void* ctx) {
        State& s = *reinterpret_cast<State*>(ctx);
        Read(s);
      },
      &s);

  for (auto& writer : writers) {
    thrd_create(
        &writer.thread,
        [](void* ctx) {
          WriterState& ws = *reinterpret_cast<WriterState*>(ctx);
          Write(*ws.state, kPayloadWords * ws.id);
        },
        &writer);
  }

  thrd_join(reader);
  for (auto& writer : writers) {
    thrd_join(writer.thread);
  }

  return 0;
}