flan_dev_result_get was not the seqlock its comment claimed
It read the generation, then a non-atomic length, then returned the buffer itself — and the agent sent those bytes down a socket some time later, while the game thread was free to be a hundred bytes into the next value. A seqlock cannot validate a read that finishes after it returns, so the pointer was the bug and not the ordering. Made into a real one rather than documented down to what it guaranteed, because what it guaranteed was nothing: the generation told the daemon a new value had arrived and said nothing about whether the bytes it then read were that value. Writing the honest comment would have left the daemon's only way of reading a result unsound with a note beside it. The counter is odd for exactly as long as a value is being written. flan_dev_result_read copies into the caller's buffer and checks the counter either side of the copy, retrying if it moved; a reader that loses the race reports the last complete generation and no bytes, so a daemon polling for a new value keeps polling rather than being shown half of one. The count handed out is the number of complete values, so "has it moved" still means what lib/dev.ml takes it to mean. The agent's buffer is RESULT_MAX, so the copy is never truncated. The race itself has no regression test. Arranging it means landing a socket read inside a render thunk from outside the process, which is the same hook the snapshot generation wants. What is tested is that eval still reads back the value it rendered, through test_dev's existing cases.
This commit is contained in:
parent
3afce2aeac
commit
8ce05087c8
@ -123,7 +123,23 @@ void *flan_dev_global(const char *name, uint64_t size, const void *init) {
|
||||
*
|
||||
* [generation] is what makes the read safe without a handshake. The thunk runs
|
||||
* on the game thread at a frame boundary, whenever that happens to be; the
|
||||
* daemon waits for the counter to move rather than guessing it has. */
|
||||
* daemon waits for the counter to move rather than guessing it has.
|
||||
*
|
||||
* It is a *seqlock*, and it has to be a real one, because the reader is the
|
||||
* agent's listener thread and the writer is the game thread and neither waits
|
||||
* for the other. The counter is odd for exactly as long as a value is being
|
||||
* written, so a reader that sees an odd count, or a different count either
|
||||
* side of its copy, has read a value that was being overwritten underneath it
|
||||
* and reads again. A count of 2k means k complete values; the count the
|
||||
* outside world is given is that k, so that the daemon's "has it moved" keeps
|
||||
* meaning "is there a new value".
|
||||
*
|
||||
* The copy is what makes it safe, and the API is shaped around that: a reader
|
||||
* gets *bytes of its own*, not a pointer into [result]. The pointer version of
|
||||
* this was the bug — it read the generation, then a length, then handed back
|
||||
* the buffer itself, and the caller sent it down a socket some time later
|
||||
* while the game thread was free to be a hundred bytes into the next value.
|
||||
* A seqlock cannot validate a read that happens after it returns. */
|
||||
|
||||
#define RESULT_MAX 4096
|
||||
static char result[RESULT_MAX];
|
||||
@ -132,6 +148,9 @@ static int result_full;
|
||||
static uint64_t generation;
|
||||
|
||||
void flan_dev_result_begin(void) {
|
||||
/* Odd first, and only then the reset: the counter has to say "in progress"
|
||||
* before the buffer stops being the value it used to be. */
|
||||
__atomic_store_n(&generation, generation + 1, __ATOMIC_RELEASE);
|
||||
result_len = 0;
|
||||
result_full = 0;
|
||||
}
|
||||
@ -208,12 +227,44 @@ void flan_dev_result_end(void) {
|
||||
memcpy(result + result_len, ell, k);
|
||||
result_len += k;
|
||||
}
|
||||
/* Last, so a reader that sees the new generation sees the whole value. */
|
||||
/* Last, and back to even, so a reader that sees the new generation sees the
|
||||
* whole value. */
|
||||
__atomic_store_n(&generation, generation + 1, __ATOMIC_RELEASE);
|
||||
}
|
||||
|
||||
const char *flan_dev_result_get(uint64_t *gen, uint64_t *len) {
|
||||
*gen = __atomic_load_n(&generation, __ATOMIC_ACQUIRE);
|
||||
*len = (uint64_t)result_len;
|
||||
return result;
|
||||
/* Copy the current value out, with the counter that says which one it is.
|
||||
*
|
||||
* Returns 1 having copied a value that was complete for the whole of the copy,
|
||||
* 0 if the game thread was in the middle of writing one — in which case [gen]
|
||||
* is the last *complete* value's number and [len] is 0, so a caller polling
|
||||
* for a new one keeps polling instead of being handed half of it. Spinning
|
||||
* here is bounded: the writer is a render thunk between frames, not a loop,
|
||||
* and the reader is the listener thread, which has nothing better to do.
|
||||
*
|
||||
* [cap] is the caller's buffer. A value longer than it is truncated, which is
|
||||
* the only failure this can have and is a clamp rather than an overrun; the
|
||||
* agent sizes its buffer at RESULT_MAX so it does not arise. */
|
||||
int flan_dev_result_read(char *dst, uint64_t cap, uint64_t *gen,
|
||||
uint64_t *len) {
|
||||
for (int attempt = 0; attempt < 64; attempt++) {
|
||||
uint64_t g1 = __atomic_load_n(&generation, __ATOMIC_ACQUIRE);
|
||||
if (g1 & 1) continue; /* a write is in progress */
|
||||
size_t n = __atomic_load_n(&result_len, __ATOMIC_RELAXED);
|
||||
if (n > RESULT_MAX) n = RESULT_MAX; /* a torn read cannot overrun */
|
||||
if ((uint64_t)n > cap) n = (size_t)cap;
|
||||
memcpy(dst, result, n);
|
||||
/* The copy must be ordered before the second read of the counter, or the
|
||||
* check is of a copy the compiler was free to make afterwards. */
|
||||
__atomic_thread_fence(__ATOMIC_ACQUIRE);
|
||||
if (__atomic_load_n(&generation, __ATOMIC_ACQUIRE) == g1) {
|
||||
*gen = g1 / 2;
|
||||
*len = (uint64_t)n;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
/* Integer division is the same answer either side of a write in progress:
|
||||
* during value k the counter is 2k-1 and k-1 are complete. */
|
||||
*gen = __atomic_load_n(&generation, __ATOMIC_ACQUIRE) / 2;
|
||||
*len = 0;
|
||||
return 0;
|
||||
}
|
||||
|
||||
11
vendor/agent/flan_agent.c
vendored
11
vendor/agent/flan_agent.c
vendored
@ -47,7 +47,13 @@ typedef void (*install_fn)(void);
|
||||
* is consistent. */
|
||||
typedef void (*call_fn)(void);
|
||||
|
||||
const char *flan_dev_result_get(uint64_t *gen, uint64_t *len);
|
||||
/* The value of the last evaluated expression, copied out under the seqlock in
|
||||
* runtime/flan_dev.c rather than borrowed. The buffer below is RESULT_MAX, so
|
||||
* the copy is never truncated; a read that loses the race reports the last
|
||||
* complete generation and no bytes, which leaves the daemon polling rather
|
||||
* than showing it half a value. */
|
||||
#define RESULT_MAX 4096
|
||||
int flan_dev_result_read(char *dst, uint64_t cap, uint64_t *gen, uint64_t *len);
|
||||
|
||||
/* A ring the listener writes and the game thread reads. One producer, one
|
||||
* consumer, so two atomics and no lock — the game thread must never block on
|
||||
@ -568,7 +574,8 @@ static void serve(int fd) {
|
||||
}
|
||||
if (strcmp(line, "result") == 0) {
|
||||
uint64_t gen = 0, len = 0;
|
||||
const char *v = flan_dev_result_get(&gen, &len);
|
||||
char v[RESULT_MAX];
|
||||
flan_dev_result_read(v, sizeof v, &gen, &len);
|
||||
char hdr[64];
|
||||
int k = snprintf(hdr, sizeof hdr, "%llu %llu\n", (unsigned long long)gen,
|
||||
(unsigned long long)len);
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user