From 8a952adf43a70ef2d1b63c5244faabd87e6fcdf9 Mon Sep 17 00:00:00 2001 From: Hung-Chun Tseng Date: Wed, 2 Sep 2026 00:52:44 +0800 Subject: [PATCH 01/11] Reject a PI waiter from any plain requeue Linux answers EINVAL when a requeue without FUTEX_CMP_REQUEUE_PI meets a waiter holding an rt_waiter or a pi_state. futex_requeue() in kernel/futex/requeue.c runs that test from inside its walk, before it decides whether the waiter in hand is woken or moved, and without consulting either address. elfuse narrowed it three ways: - it required uaddr != uaddr2, though only the requeue_pi form rejects uaddr1 == uaddr2 as such, so a requeue onto the waiter's own address reported a moved count; - it skipped the first wake_count matches, so a PI waiter inside the wake budget was woken rather than refused; - it ran only when requeue_count was non-zero, so a wake-only requeue never looked at all. The first also outlived the call. That rejection is what keeps the published waiter census #348 added away from a PI waiter, whose bucket charge futex_lock_pi's wrapper owns for the whole call. Letting one through ran the charge move, which credits the destination but debits w->pub_bucket only under pub_follows, so the bucket kept a charge for a waiter that had gone and futex_wake_fast read it as occupied from then on. Repeat the call and the uint32 count wraps, and a zero reading is a wake answered at EL1 while a waiter is parked. Walk every waiter the call could act on instead, bounded by wake_count + requeue_count the way Linux's own "task_count - nr_wake >= nr_requeue" break bounds it. The sum is taken in 64 bits because both halves are guest-supplied and wake-all passes INT_MAX. The sibling guard from the same function comes with it: Linux opens futex_requeue() on "nr_wake < 0 || nr_requeue < 0" before it takes either key. Both counts arrive here as uint32_t -- nr_wake from sc_futex's (uint32_t) x2, nr_requeue out of the timeout slot -- so the sign only survives as the top bit, and reading them back as int32_t is what recovers it. Without it futex(X, FUTEX_REQUEUE, -1, -1, Y) was a wake-all and requeue-all where Linux answers EINVAL. Both halves of the charge move go under pub_follows as well. It is unreachable for a PI waiter now, but a credit sitting outside the branch that carries its debit is what let the two come apart, and pairing them keeps a later narrowing of the guard from reintroducing it. tests/test-futex-requeue-pi.c parks a PI waiter in FUTEX_LOCK_PI and puts one case to each narrowing, retrying the first while the call reports zero because that is its answer before the waiter parks. Two more cases hold the negative counts, which need no waiter: on an empty address the wake and the requeue are both no-ops, so the zero an unguarded build reports is what the assertion separates EINVAL from. Every assertion is an errno, so the matrix can put the same source to a reference kernel, and every op carries FUTEX_PRIVATE_FLAG for that reason: elfuse masks the bit off in FUTEX_CMD_MASK, but on a real kernel private and shared hash to different keys, and without it the parking and the closing raw_futex_wake -- which sets the flag -- would name two different futexes, leaving the drained-address check to pass for free. The census needs none: an over-count is invisible from the guest, because the host answers every wake correctly either way, and the restored rejection makes it unreachable. The holder reports a refused FUTEX_LOCK_PI rather than leaving the handshake unset. main and the waiter both wait on holder_ready with no deadline, so a tree whose LOCK_PI does not work -- the one this lane exists to catch -- wedged the suite instead of failing it. Measured against LOCK_PI stubbed to ENOSYS: a 60 second cap reached with no output at all before, exit 1 inside a second now, naming the refusal. The EXPECTED_BASELINES floors are left alone. The matrix lane wants aarch64-none-elf-as for tests/hello.S, which this machine cannot install, so a raised floor would be a number nobody observed. --- src/runtime/futex.c | 59 +++++----- tests/test-futex-requeue-pi.c | 207 ++++++++++++++++++++++++++++++++++ tests/test-matrix.sh | 2 + 3 files changed, 239 insertions(+), 29 deletions(-) create mode 100644 tests/test-futex-requeue-pi.c diff --git a/src/runtime/futex.c b/src/runtime/futex.c index 7dc72a7f..ceb7cbd4 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -1409,6 +1409,12 @@ static int64_t futex_requeue(guest_t *g, int do_cmp, uint32_t expected) { + /* Linux refuses these before taking either key. Both arrive as uint32_t, so + * the guest's sign survives only as the top bit. + */ + if ((int32_t) wake_count < 0 || (int32_t) requeue_count < 0) + return -LINUX_EINVAL; + if (!futex_uaddr_is_aligned(uaddr) || !futex_uaddr_is_aligned(uaddr2)) return -LINUX_EINVAL; @@ -1439,34 +1445,28 @@ static int64_t futex_requeue(guest_t *g, } } - /* A PI waiter remains tied to its entry bucket while it retries the PI - * acquisition. FUTEX_REQUEUE has no PI-aware counterpart here, so reject an - * attempted migration before waking or moving any waiter. + /* A PI waiter stays tied to its entry bucket while it retries, and + * FUTEX_REQUEUE has no PI-aware form here, so reject one before anything + * moves. Every waiter the call could touch is checked, wake candidates + * included, matching where requeue.c makes the same decision. The budget is + * summed in 64 bits: both halves are guest-supplied and wake-all passes + * INT_MAX. */ - if (uaddr != uaddr2 && requeue_count != 0) { - uint32_t skips = wake_count; - uint32_t remaining = requeue_count; - - for (futex_waiter_t *w = b_src->head; w; w = w->next) { - if (w->uaddr != uaddr) - continue; - if (skips != 0) { - skips--; - continue; - } + uint64_t checked = (uint64_t) wake_count + requeue_count; + for (futex_waiter_t *w = b_src->head; w && checked != 0; w = w->next) { + if (w->uaddr != uaddr) + continue; - /* pub_follows is false only for a PI waiter today; see where it is - * set in futex_lock_pi_inner. - */ - if (!w->pub_follows) { - if (idx_src != idx_dst) - pthread_mutex_unlock(&b_dst->lock); - pthread_mutex_unlock(&b_src->lock); - return -LINUX_EINVAL; - } - if (--remaining == 0) - break; + /* pub_follows is false only for a PI waiter today; see where it is set + * in futex_lock_pi_inner. + */ + if (!w->pub_follows) { + if (idx_src != idx_dst) + pthread_mutex_unlock(&b_dst->lock); + pthread_mutex_unlock(&b_src->lock); + return -LINUX_EINVAL; } + checked--; } int woken = 0, requeued = 0; @@ -1489,12 +1489,13 @@ static int64_t futex_requeue(guest_t *g, /* Requeue: remove from source, add to destination */ *pp = w->next; - /* Move the publication with the waiter. The destination is charged - * before the source is debited, so the shim never sees this parked - * waiter charged to no bucket. + /* Credit the destination before debiting the source, so the shim + * never sees this waiter charged to no bucket. Both halves sit + * under pub_follows: a waiter carrying no charge of its own must + * not gain one here, which is how a charge outlived its waiter. */ - shim_globals_futex_waiters_add(g, idx_dst, +1); if (w->pub_follows) { + shim_globals_futex_waiters_add(g, idx_dst, +1); shim_globals_futex_waiters_add(g, w->pub_bucket, -1); w->pub_bucket = idx_dst; } diff --git a/tests/test-futex-requeue-pi.c b/tests/test-futex-requeue-pi.c new file mode 100644 index 00000000..83b62cf1 --- /dev/null +++ b/tests/test-futex-requeue-pi.c @@ -0,0 +1,207 @@ +/* + * A plain FUTEX_REQUEUE must refuse a PI waiter, whatever the addresses are + * + * Copyright 2026 elfuse contributors + * SPDX-License-Identifier: Apache-2.0 + * + * Linux answers EINVAL when a requeue without FUTEX_CMP_REQUEUE_PI meets a + * waiter holding an rt_waiter or a pi_state. The test is on the waiter alone, + * so neither the addresses nor the wake budget excuses one, and this file puts + * a case to each of those. It also holds the negative counts requeue.c refuses + * before it takes either key. + * + * The requeue is retried while it reports zero, which is the answer when nobody + * is parked yet: without that loop a slow thread start would pass by never + * reaching the case. + * + * Syscalls exercised: futex(98), clone(220), gettid(178), exit(93), sched_yield + */ + +#include +#include +#include +#include +#include + +#include "test-harness.h" +#include "raw-syscall.h" + +int passes = 0, fails = 0; + +/* The lock under test and the four handshake words that sequence the two + * threads around it. + */ +static int pi_lock; /* the PI futex the waiter parks on */ +static int holder_ready; /* set once the holder has settled, either way */ +static int holder_failed; /* set instead of owning it, when LOCK_PI refused */ +static int release; /* set to tell the holder to unlock */ +static int waiter_done; /* set once the waiter has taken and released it */ + +static int holder_stack[16384] __attribute__((aligned(16))); +static int waiter_stack[16384] __attribute__((aligned(16))); + +/* Every op carries FUTEX_PRIVATE_FLAG, as the neighbouring futex tests do. + * elfuse masks it off, but on a reference kernel private and shared hash to + * different keys, and raw_futex_wake sets it. + */ +static long futex_lock_pi(int *addr) +{ + return raw_syscall6(__NR_futex, (long) addr, + FUTEX_LOCK_PI | FUTEX_PRIVATE_FLAG, 0, 0, 0, 0); +} + +static long futex_unlock_pi(int *addr) +{ + return raw_syscall6(__NR_futex, (long) addr, + FUTEX_UNLOCK_PI | FUTEX_PRIVATE_FLAG, 0, 0, 0, 0); +} + +/* FUTEX_REQUEUE reads its requeue count out of the timeout slot. */ +static long futex_requeue_same(int *addr, long wake, long requeue) +{ + return raw_syscall6(__NR_futex, (long) addr, + FUTEX_REQUEUE | FUTEX_PRIVATE_FLAG, wake, requeue, + (long) addr, 0); +} + +static void set_and_wake(int *addr) +{ + __atomic_store_n(addr, 1, __ATOMIC_RELEASE); + raw_futex_wake(addr, 1); +} + +static void wait_until_set(int *addr) +{ + while (__atomic_load_n(addr, __ATOMIC_ACQUIRE) == 0) + raw_futex_wait(addr, 0); +} + +/* Takes pi_lock, reports it, and holds it until told to let go. The waiter + * cannot park until someone else owns the word. + */ +static void holder_fn(void) +{ + if (futex_lock_pi(&pi_lock) == 0) { + set_and_wake(&holder_ready); + wait_until_set(&release); + futex_unlock_pi(&pi_lock); + } else { + /* Say so rather than leave main parked on holder_ready forever: a tree + * whose LOCK_PI is broken is the one this lane exists to catch. + */ + set_and_wake(&holder_failed); + set_and_wake(&holder_ready); + } + raw_exit(0); +} + +/* Parks in FUTEX_LOCK_PI on the held word. This is the waiter whose charge the + * requeue must not move, and the one whose bucket is left over-counted. + */ +static void waiter_fn(void) +{ + wait_until_set(&holder_ready); + if (futex_lock_pi(&pi_lock) == 0) + futex_unlock_pi(&pi_lock); + set_and_wake(&waiter_done); + raw_exit(0); +} + +int main(void) +{ + /* CLONE_VM | CLONE_FS | CLONE_FILES | CLONE_SIGHAND | CLONE_THREAD | + * CLONE_SYSVSEM, spelled as the value the way test-futex-pi.c does. No TLS + * or tid flags: a CHILD_CLEARTID wake would only add futex traffic. + */ + unsigned long flags = 0x50f00; + + printf("=== futex requeue PI rejection tests ===\n\n"); + + /* No waiter needed: on an empty address both counts are no-ops, so the zero + * an unguarded build reports is what EINVAL separates from. + */ + TEST("a negative wake count is EINVAL"); + EXPECT_RAW_ERRNO(futex_requeue_same(&pi_lock, -1, 0), -EINVAL, + "a negative wake count must be refused"); + + TEST("a negative requeue count is EINVAL"); + EXPECT_RAW_ERRNO(futex_requeue_same(&pi_lock, 0, -1), -EINVAL, + "a negative requeue count must be refused"); + + /* One clone at a time, each with its child branch immediately after it: + * issuing both first lets the first child run the second raw_clone too. + * test-thread.c and test-futex-pi.c clone this way for the same reason. + */ + TEST("clone holder and waiter"); + long holder = raw_clone(flags, holder_stack + 16384, 0, 0, 0); + if (holder == 0) { + holder_fn(); + __builtin_unreachable(); + } + if (holder < 0) { + FAIL("holder clone failed"); + goto done; + } + + long waiter = raw_clone(flags, waiter_stack + 16384, 0, 0, 0); + if (waiter == 0) { + waiter_fn(); + __builtin_unreachable(); + } + if (waiter < 0) { + FAIL("waiter clone failed"); + goto done; + } + PASS(); + + wait_until_set(&holder_ready); + + TEST("holder takes pi_lock"); + if (__atomic_load_n(&holder_failed, __ATOMIC_ACQUIRE) != 0) { + FAIL("FUTEX_LOCK_PI refused the holder, nothing to requeue against"); + goto done; + } + PASS(); + + /* Zero is the answer before the waiter parks; anything else means the call + * saw it, and EINVAL is the only correct one. + */ + TEST("requeue a parked PI waiter onto its own address"); + long rc = 0; + for (int i = 0; i < 100000 && rc == 0; i++) { + rc = futex_requeue_same(&pi_lock, 0, 1); + if (rc == 0) + raw_syscall0(__NR_sched_yield); + } + EXPECT_RAW_ERRNO(rc, -EINVAL, "requeuing a PI waiter must be EINVAL"); + + /* Still parked, so the other two shapes reuse it. The check outranks the + * wake/requeue decision, so neither budget excuses a PI waiter. + */ + TEST("PI waiter inside the wake budget"); + EXPECT_RAW_ERRNO(futex_requeue_same(&pi_lock, 1, 1), -EINVAL, + "a PI waiter within wake_count must be EINVAL, not woken"); + + TEST("wake-only requeue with a PI waiter"); + EXPECT_RAW_ERRNO(futex_requeue_same(&pi_lock, 1, 0), -EINVAL, + "requeue_count 0 does not excuse a PI waiter"); + + set_and_wake(&release); + wait_until_set(&waiter_done); + + /* Nobody is parked now, so a rejected requeue must not have left the waiter + * somewhere a later wake still finds. + */ + TEST("wake the drained address"); + for (int i = 0; i < 8; i++) { + if (raw_futex_wake(&pi_lock, 1) != 0) { + FAIL("a drained address reported a woken waiter"); + goto done; + } + } + PASS(); + +done: + SUMMARY("test-futex-requeue-pi"); + return fails > 0 ? 1 : 0; +} diff --git a/tests/test-matrix.sh b/tests/test-matrix.sh index 840033a5..d9970e27 100755 --- a/tests/test-matrix.sh +++ b/tests/test-matrix.sh @@ -892,6 +892,8 @@ run_unit_tests() "$bindir/test-futex-wake-nowaiter" test_rc "$runner" "test-futex-requeue-account" 0 \ "$bindir/test-futex-requeue-account" + test_rc "$runner" "test-futex-requeue-pi" 0 \ + "$bindir/test-futex-requeue-pi" test_rc "$runner" "test-robust-futex" 0 "$bindir/test-robust-futex" test_check "$runner" "test-shim-futex-fast" "OK" \ "$bindir/test-shim-futex-fast" From 0f2d7fcaedf20991443443d2b7e81f64448c6bc4 Mon Sep 17 00:00:00 2001 From: alanhc Date: Wed, 2 Sep 2026 18:38:29 +0800 Subject: [PATCH 02/11] Prove the requeue count contract The negative-count guard added with the PI rejection is arithmetic over two guest-supplied words, which is the shape src/proved holds. It moves there as futexreq.h, alongside the futexhash and futexop fragments the same syscall already has, and make verify-futexreq discharges it. Two functions carry it. futex_requeue_counts_valid states the rule Linux applies before it takes either key, and futex_requeue_budget states what the walk is then bounded by. The second has the first as a precondition, which is the part worth proving: a validated pair leaves the sum inside 32 bits, where an unvalidated one bounds the walk at 2^33 - 2. That is the overflow CVE-2018-6927 reached, through this same argument pair on this same syscall; futexop.h already names it next door. The test is now a comparison against 2^31 rather than a cast back to int32_t. Converting a value above INT32_MAX to a signed type is implementation-defined before C23, so the cast was reading a sign the standard does not promise, and the provers stay in the value theory without it -- the reason futexop.h and futexhash.h spell their masks as remainders. No behavior changes: test-futex-requeue-pi still reports 8 passed, 0 failed under elfuse and against Linux 6.18.44 in the qemu lane. --- mk/verify.mk | 9 +++++++ src/proved/futexreq.h | 59 +++++++++++++++++++++++++++++++++++++++++++ src/runtime/futex.c | 9 ++++--- 3 files changed, 73 insertions(+), 4 deletions(-) create mode 100644 src/proved/futexreq.h diff --git a/mk/verify.mk b/mk/verify.mk index 9d121021..02390dec 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -391,6 +391,15 @@ VERIFY_FUTEXOP_SCAN := src/proved/futexop.h VERIFY_FUTEXOP_CLAIM := for ANY guest-supplied val3 word VERIFY_FUTEXOP_UNPROVED := the wake and requeue walks around them stay test-covered +VERIFY_FUTEXREQ_SRC := src/proved/futexreq.h +VERIFY_FUTEXREQ_FCTS := futex_requeue_counts_valid futex_requeue_budget +VERIFY_FUTEXREQ_MIN_GOALS ?= 14 +# typed: two scalars in, one out, no buffer and no aliasing question. +VERIFY_FUTEXREQ_MODEL := typed +VERIFY_FUTEXREQ_SCAN := src/proved/futexreq.h +VERIFY_FUTEXREQ_CLAIM := for ANY pair of guest-supplied requeue counts +VERIFY_FUTEXREQ_UNPROVED := the bucket walk the budget bounds stays test-covered + VERIFY_PATHDEPTH_SRC := src/proved/pathdepth.h VERIFY_PATHDEPTH_FCTS := path_depth_push path_depth_pop VERIFY_PATHDEPTH_MIN_GOALS ?= 24 diff --git a/src/proved/futexreq.h b/src/proved/futexreq.h new file mode 100644 index 00000000..6154e8d7 --- /dev/null +++ b/src/proved/futexreq.h @@ -0,0 +1,59 @@ +/* + * Requeue count validation, split out of futex_requeue in src/runtime/futex.c + * and proved here. + * + * Linux refuses a plain FUTEX_REQUEUE whose wake or requeue count is negative, + * before it takes either futex key. The counts reach elfuse as uint32_t -- + * sc_futex forwards val as (uint32_t) x2 and the requeue half out of the + * timeout slot -- so the sign the guest passed survives only as the top bit. + * + * The test compares against 2^31 rather than casting back to int32_t. + * Converting a value above INT32_MAX to a signed type is implementation-defined + * before C23, and the provers reason about the unsigned value directly, the way + * futexop.h and futexhash.h stay in the value theory for the same reason. + * + * Validation has to come first because of the budget below: the walk stops once + * it has touched nr_wake + nr_requeue waiters, and a negative pair read as + * unsigned makes that bound 2^33 - 2. Refusing the pair is what holds the sum + * inside 32 bits. The overflow CVE-2018-6927 reached went through this same + * argument pair, on the same syscall. + */ +#pragma once + +#include + +/* One past the largest count a guest can pass as a non-negative int32_t. */ +#define FUTEX_COUNT_LIMIT 0x80000000u + +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: + \result != 0 <==> (nr_wake < 0x80000000 && nr_requeue < 0x80000000); + */ +static inline int futex_requeue_counts_valid(uint32_t nr_wake, + uint32_t nr_requeue) +{ + return nr_wake < FUTEX_COUNT_LIMIT && nr_requeue < FUTEX_COUNT_LIMIT; +} + +/* How many waiters the call may touch. Linux bounds its walk the same way, by + * breaking once task_count reaches nr_wake + nr_requeue. + * + * The sum is taken in 64 bits so the addition itself cannot wrap whatever the + * caller passes; no_overflow is the stronger statement, that a validated pair + * leaves the result inside 32 bits. + */ +/*@ + requires valid: nr_wake < 0x80000000 && nr_requeue < 0x80000000; + assigns \nothing; + ensures sum: \result == (uint64_t) nr_wake + nr_requeue; + ensures covers_wake: \result >= nr_wake; + ensures covers_requeue: \result >= nr_requeue; + ensures no_overflow: \result < 0x100000000; + */ +static inline uint64_t futex_requeue_budget(uint32_t nr_wake, + uint32_t nr_requeue) +{ + return (uint64_t) nr_wake + nr_requeue; +} diff --git a/src/runtime/futex.c b/src/runtime/futex.c index ceb7cbd4..a275287b 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -42,6 +42,7 @@ #include "debug/log.h" #include "proved/futexhash.h" #include "proved/futexop.h" +#include "proved/futexreq.h" #include "proved/timespec.h" /* macOS 14.4+ ships os_sync_{wait_on_address_with_timeout,wake_by_address_any} @@ -1409,10 +1410,10 @@ static int64_t futex_requeue(guest_t *g, int do_cmp, uint32_t expected) { - /* Linux refuses these before taking either key. Both arrive as uint32_t, so - * the guest's sign survives only as the top bit. + /* Linux refuses these before taking either key; proved/futexreq.h carries + * why the sign is only visible as the top bit here. */ - if ((int32_t) wake_count < 0 || (int32_t) requeue_count < 0) + if (!futex_requeue_counts_valid(wake_count, requeue_count)) return -LINUX_EINVAL; if (!futex_uaddr_is_aligned(uaddr) || !futex_uaddr_is_aligned(uaddr2)) @@ -1452,7 +1453,7 @@ static int64_t futex_requeue(guest_t *g, * summed in 64 bits: both halves are guest-supplied and wake-all passes * INT_MAX. */ - uint64_t checked = (uint64_t) wake_count + requeue_count; + uint64_t checked = futex_requeue_budget(wake_count, requeue_count); for (futex_waiter_t *w = b_src->head; w && checked != 0; w = w->next) { if (w->uaddr != uaddr) continue; From 415cb2cdbcd32f488e98e26051f24975b6e3c09c Mon Sep 17 00:00:00 2001 From: Hung-Chun Tseng Date: Wed, 2 Sep 2026 20:16:59 +0800 Subject: [PATCH 03/11] Make the futexreq gate bite verify-mutants runs per target, and a target with no entry in MUTATIONS exits 2 rather than passing vacuously: "no mutations for target 'futexreq'". Adding VERIFY_FUTEXREQ_* put futexreq in the CI matrix without giving it one, so the Mutations lane fails and the Frama-C gate that requires both halves fails with it. Two entries, one per proved function, both confirmed to make a goal go UNPROVED rather than to trip the MIN_GOALS floor. futex_requeue_counts_valid accepts every pair, which breaks the <==> in its exact clause: the result is then 1 for arguments the right-hand side excludes. futex_requeue_budget returns the requeue half alone, which breaks covers_wake. The obvious mutation there is not this one, and it does not work: adding in 32 bits before the widening cast leaves the result unchanged, because requires valid already bounds both arguments below 2^31 and their sum cannot wrap. That the cast is unnecessary under the precondition is the contract doing its job, so the mutation has to attack a clause the precondition does not already settle. Measured, not reasoned: the 32-bit form was tried first and reported MISSED. Verified with the versions the workflow pins, Frama-C 33.0, Alt-Ergo 2.6.3 and Z3 4.16.0: verify-futexreq proves 14 of 14 unmutated, and verify-mutants MUTANT_TARGET=futexreq reports 2 mutations, 2 caught. --- scripts/check-mutants.py | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 7b083a6b..0e4c08c9 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -179,6 +179,23 @@ def _load(stem, name): " FUTEX_TIMESPEC_SEC_MAX);\n", " return lts->tv_sec >= 0 && lts->tv_nsec >= 0;\n", ), + # ---- verify-futexreq --------------------------------------------------- + ( + "futexreq", + "src/proved/futexreq.h", + "futex_requeue_counts_valid", + "accept any pair (a negative count survives as a huge unsigned)", + " return nr_wake < FUTEX_COUNT_LIMIT && nr_requeue < FUTEX_COUNT_LIMIT;\n", + " return 1;\n", + ), + ( + "futexreq", + "src/proved/futexreq.h", + "futex_requeue_budget", + "bound the walk by the requeue half alone (the wake budget goes unwalked)", + " return (uint64_t) nr_wake + nr_requeue;\n", + " return (uint64_t) nr_requeue;\n", + ), # ---- verify-futexop ---------------------------------------------------- ( "futexop", From b92aede20ee808929c0d3fa645ad3b65b710c6e9 Mon Sep 17 00:00:00 2001 From: alanhc Date: Wed, 2 Sep 2026 22:06:02 +0800 Subject: [PATCH 04/11] Refuse an unassigned FUTEX_WAKE_OP selector Both selectors in the val3 word of a FUTEX_WAKE_OP call are guest supplied, and both have encodings Linux does not implement. It answers ENOSYS for those. elfuse treated them as no-ops: an unhandled op left the word alone and an unhandled comparison left the condition false, after which the call went on to wake up to nr_wake waiters at uaddr and report the count. Linux refuses each at a different point, and the modify makes the difference visible. futex_atomic_op_inuser() checks the op inside arch_futex_atomic_op_inuser(), before the read-modify-write, and the comparison after it. Neither reaches a wake. Measured on the reference kernel this tree cross-checks against, Linux 6.18.44 through the qemu lane, with one waiter parked on uaddr: op cmp ret *uaddr2 waiter SET EQ 0 or 1 modified woken 5..7 EQ -ENOSYS untouched parked SET 6, 15 -ENOSYS modified parked elfuse now answers the same in every column. The op gate sits with the operand decode, which already returned before the buckets are locked, so it needs no unlock path of its own. The comparison gate is after the CAS loop and takes the two unlocks the EFAULT return beside it takes. The selectors and the two switches they guard move to src/proved/futexwakeop.h, where WP discharges 92 obligations. The postconditions pin one value per op rather than a range, so the body that returned old_val for an unhandled op no longer satisfies them. ANDN casts its complement back to uint32_t in the contract: ACSL reads ~x as -x-1, and relating a negative operand of & to the code times out on both provers at 30s. That is the same wall futexop.h documents for the bitwise forms it avoids. tests/test-futex-wake-op-enosys.c puts a case to each row above and passes unchanged on the reference kernel. It lives in test-matrix.sh's run_unit_tests and not in tests/manifest.txt, per that file's scope note: every assertion is an errno or a word the guest can read, so it is cross-checkable rather than elfuse-internal. The waiter cases retry on EINTR rather than counting it as a wake. elfuse can return EINTR from a FUTEX_WAIT no signal was delivered to, which a first draft of the test read as the refused call answering it. --- mk/verify.mk | 10 ++ src/proved/futexwakeop.h | 111 +++++++++++++++ src/runtime/futex.c | 66 +++------ tests/test-futex-wake-op-enosys.c | 226 ++++++++++++++++++++++++++++++ tests/test-matrix.sh | 2 + 5 files changed, 369 insertions(+), 46 deletions(-) create mode 100644 src/proved/futexwakeop.h create mode 100644 tests/test-futex-wake-op-enosys.c diff --git a/mk/verify.mk b/mk/verify.mk index 02390dec..fd61828d 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -400,6 +400,16 @@ VERIFY_FUTEXREQ_SCAN := src/proved/futexreq.h VERIFY_FUTEXREQ_CLAIM := for ANY pair of guest-supplied requeue counts VERIFY_FUTEXREQ_UNPROVED := the bucket walk the budget bounds stays test-covered +VERIFY_FUTEXWAKEOP_SRC := src/proved/futexwakeop.h +VERIFY_FUTEXWAKEOP_FCTS := futex_wake_op_supported futex_wake_cmp_supported \ + futex_wake_op_apply futex_wake_op_cmp +VERIFY_FUTEXWAKEOP_MIN_GOALS ?= 92 +# typed: scalars in, one scalar out, no buffer and no aliasing question. +VERIFY_FUTEXWAKEOP_MODEL := typed +VERIFY_FUTEXWAKEOP_SCAN := src/proved/futexwakeop.h +VERIFY_FUTEXWAKEOP_CLAIM := for ANY guest-supplied op and comparison selector +VERIFY_FUTEXWAKEOP_UNPROVED := the wake walks the selectors gate stay test-covered + VERIFY_PATHDEPTH_SRC := src/proved/pathdepth.h VERIFY_PATHDEPTH_FCTS := path_depth_push path_depth_pop VERIFY_PATHDEPTH_MIN_GOALS ?= 24 diff --git a/src/proved/futexwakeop.h b/src/proved/futexwakeop.h new file mode 100644 index 00000000..606a80df --- /dev/null +++ b/src/proved/futexwakeop.h @@ -0,0 +1,111 @@ +/* + * Operation and comparison selectors for FUTEX_WAKE_OP, split out of + * futex_wake_op in src/runtime/futex.c and proved here. + * + * Both selectors are guest-supplied and both have unassigned encodings. Linux + * answers ENOSYS for those, and refuses each at a different point: an op it + * does not implement stops before the read-modify-write, an unimplemented + * comparison stops after it. Neither wakes anybody. The measurements behind + * that split are in the commit message. + * + * The selectors are compared against their bounds rather than enumerated, so + * the supported set stays one number per side. + */ +#pragma once + +#include + +/* Largest selector Linux implements: FUTEX_OP_XOR and FUTEX_OP_CMP_GE. */ +#define FUTEX_WAKE_OP_MAX 4u +#define FUTEX_WAKE_CMP_MAX 5u + +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: \result != 0 <==> op <= 4; + */ +static inline int futex_wake_op_supported(uint32_t op) +{ + return op <= FUTEX_WAKE_OP_MAX; +} + +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: \result != 0 <==> cmp <= 5; + */ +static inline int futex_wake_cmp_supported(uint32_t cmp) +{ + return cmp <= FUTEX_WAKE_CMP_MAX; +} + +/* The word uaddr2 takes. Every op is modular, so a sign-extended operand is + * carried as its two's complement bits. + * + * The postconditions pin a value per op rather than a range: a body that + * returned old_val throughout, which is what an unhandled op used to do, meets + * a range and fails these. + * + * ANDN casts its complement back to uint32_t. Without the cast ACSL reads ~x as + * -x-1, and relating a negative operand of & to the code times out. + */ +/*@ + requires supported: op <= 4; + assigns \nothing; + ensures set: op == 0 ==> \result == op_val; + ensures add: op == 1 ==> \result == (uint32_t) (old_val + op_val); + ensures or: op == 2 ==> \result == (old_val | op_val); + ensures andn: op == 3 ==> \result == (old_val & (uint32_t) ~op_val); + ensures xor: op == 4 ==> \result == (old_val ^ op_val); + */ +static inline uint32_t futex_wake_op_apply(uint32_t old_val, + uint32_t op, + uint32_t op_val) +{ + switch (op) { + case 0: + return op_val; + case 1: + return old_val + op_val; + case 2: + return old_val | op_val; + case 3: + return old_val & ~op_val; + default: + return old_val ^ op_val; + } +} + +/* Whether the second wake fires. The comparisons are signed, on the word as it + * was before the modify above. + */ +/*@ + requires supported: cmp <= 5; + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures eq: cmp == 0 ==> (\result != 0 <==> old_val == cmp_arg); + ensures ne: cmp == 1 ==> (\result != 0 <==> old_val != cmp_arg); + ensures lt: cmp == 2 ==> (\result != 0 <==> old_val < cmp_arg); + ensures le: cmp == 3 ==> (\result != 0 <==> old_val <= cmp_arg); + ensures gt: cmp == 4 ==> (\result != 0 <==> old_val > cmp_arg); + ensures ge: cmp == 5 ==> (\result != 0 <==> old_val >= cmp_arg); + */ +static inline int futex_wake_op_cmp(int32_t old_val, + uint32_t cmp, + int32_t cmp_arg) +{ + switch (cmp) { + case 0: + return old_val == cmp_arg; + case 1: + return old_val != cmp_arg; + case 2: + return old_val < cmp_arg; + case 3: + return old_val <= cmp_arg; + case 4: + return old_val > cmp_arg; + default: + return old_val >= cmp_arg; + } +} diff --git a/src/runtime/futex.c b/src/runtime/futex.c index a275287b..6f156e7d 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -43,6 +43,7 @@ #include "proved/futexhash.h" #include "proved/futexop.h" #include "proved/futexreq.h" +#include "proved/futexwakeop.h" #include "proved/timespec.h" /* macOS 14.4+ ships os_sync_{wait_on_address_with_timeout,wake_by_address_any} @@ -1587,6 +1588,12 @@ static int64_t futex_wake_op(guest_t *g, op_val = 1U << futex_op_shift_arg_mask(op_arg); wake_op &= 7; /* Actual operation is bits 0-2 */ + /* An op Linux does not implement stops here, before the modify and before + * any wake. proved/futexwakeop.h carries both gates. + */ + if (!futex_wake_op_supported(wake_op)) + return -LINUX_ENOSYS; + unsigned idx1 = futex_hash(uaddr); unsigned idx2 = futex_hash(uaddr2); futex_bucket_t *b1 = &buckets[idx1]; @@ -1622,26 +1629,7 @@ static int64_t futex_wake_op(guest_t *g, ok = futex_word_load(word2, &old_val); if (!ok) break; - switch (wake_op) { - case 0: - new_val = op_val; - break; /* SET */ - case 1: - new_val = old_val + op_val; - break; /* ADD */ - case 2: - new_val = old_val | op_val; - break; /* OR */ - case 3: - new_val = old_val & ~op_val; - break; /* ANDN */ - case 4: - new_val = old_val ^ op_val; - break; /* XOR */ - default: - new_val = old_val; - break; - } + new_val = futex_wake_op_apply(old_val, wake_op, op_val); ok = futex_word_cas(word2, &old_val, new_val, &swapped); } while (ok && !swapped); @@ -1652,6 +1640,16 @@ static int64_t futex_wake_op(guest_t *g, return -LINUX_EFAULT; } + /* A comparison Linux does not implement stops here: the modify above has + * already landed, and neither wake runs. + */ + if (!futex_wake_cmp_supported(wake_cmp)) { + if (idx1 != idx2) + pthread_mutex_unlock(&b2->lock); + pthread_mutex_unlock(&b1->lock); + return -LINUX_ENOSYS; + } + /* Wake up to val waiters at uaddr (unlink woken entries) */ int woken1 = 0; futex_waiter_t **pp1 = &b1->head; @@ -1665,32 +1663,8 @@ static int64_t futex_wake_op(guest_t *g, } } - /* Evaluate comparison predicate on old_val */ - int cond_met = 0; - /* Linux FUTEX_WAKE_OP uses signed comparison semantics */ - int32_t sv = (int32_t) old_val; - switch (wake_cmp) { - case 0: - cond_met = (sv == cmp_arg); - break; /* EQ */ - case 1: - cond_met = (sv != cmp_arg); - break; /* NE */ - case 2: - cond_met = (sv < cmp_arg); - break; /* LT (signed) */ - case 3: - cond_met = (sv <= cmp_arg); - break; /* LE (signed) */ - case 4: - cond_met = (sv > cmp_arg); - break; /* GT (signed) */ - case 5: - cond_met = (sv >= cmp_arg); - break; /* GE (signed) */ - default: - break; - } + /* Signed comparison on the word as it was before the modify. */ + int cond_met = futex_wake_op_cmp((int32_t) old_val, wake_cmp, cmp_arg); /* Conditionally wake up to val2 waiters at uaddr2 (unlink woken) */ int woken2 = 0; diff --git a/tests/test-futex-wake-op-enosys.c b/tests/test-futex-wake-op-enosys.c new file mode 100644 index 00000000..00a4d632 --- /dev/null +++ b/tests/test-futex-wake-op-enosys.c @@ -0,0 +1,226 @@ +/* + * FUTEX_WAKE_OP must answer ENOSYS for a selector Linux does not implement + * + * Copyright 2026 elfuse contributors + * SPDX-License-Identifier: Apache-2.0 + * + * Both selectors in val3 are guest-supplied and both have unassigned encodings. + * Linux refuses each at a different point, which the modify makes visible: an + * unimplemented op stops before it, an unimplemented comparison after it. + * Neither wakes anybody. + * + * Every assertion is an errno or a word the guest can read, so the same source + * runs against a reference kernel. + * + * Syscalls exercised: futex(98), clone(220), exit(93), sched_yield(124) + */ + +#include +#include + +#include "test-harness.h" +#include "raw-syscall.h" + +int passes = 0, fails = 0; + +static int park_word; /* the address the waiter parks on */ +static int target_word; /* the address the modify lands on */ +static int waiter_parking; /* set just before the waiter enters FUTEX_WAIT */ +static int waiter_done; /* set once FUTEX_WAIT has returned for real */ + +static int waiter_stack[16384] __attribute__((aligned(16))); + +/* val3 layout: bit 31 OPARG_SHIFT, 30-28 op, 27-24 cmp, 23-12 oparg, 11-0 + * cmparg. + */ +static uint32_t encode(unsigned op, + unsigned cmp, + uint32_t oparg, + uint32_t cmparg) +{ + return ((op & 7u) << 28) | ((cmp & 0xfu) << 24) | ((oparg & 0xfffu) << 12) | + (cmparg & 0xfffu); +} + +/* FUTEX_WAKE_OP reads its second wake count out of the timeout slot. */ +static long futex_wake_op(long nr_wake, long nr_wake2, uint32_t val3) +{ + return raw_syscall6(__NR_futex, (long) &park_word, + FUTEX_WAKE_OP | FUTEX_PRIVATE_FLAG, nr_wake, nr_wake2, + (long) &target_word, (long) val3); +} + +/* SET 0x111, compared EQ against 0x111. The modify always lands; the compare is + * against the word as it was before, so the second wake does not fire. + */ +static uint32_t valid_val3(void) +{ + return encode(0, 0, 0x111, 0x111); +} + +static void set_and_wake(int *addr) +{ + __atomic_store_n(addr, 1, __ATOMIC_RELEASE); + raw_futex_wake(addr, 1); +} + +/* Parks once. EINTR is a retry rather than a wake, so a build that interrupts + * the wait does not read as one that answered it. + */ +static void waiter_fn(void) +{ + long r; + set_and_wake(&waiter_parking); + do { + r = raw_futex_wait(&park_word, 0); + } while (r == -EINTR); + set_and_wake(&waiter_done); + raw_exit(0); +} + +static int parked(void) +{ + return __atomic_load_n(&waiter_done, __ATOMIC_ACQUIRE) == 0; +} + +/* Give a wake that should not have happened room to arrive. A real one lands + * within a few yields; this is generous rather than tuned. + */ +static void settle(void) +{ + for (int i = 0; i < 10000; i++) + raw_syscall0(__NR_sched_yield); +} + +/* No waiter is needed for the errno and the modify: on an empty address both + * wake counts are no-ops. + */ +static void unsupported_op_case(const char *name, unsigned op) +{ + TEST(name); + __atomic_store_n(&target_word, 0, __ATOMIC_RELEASE); + long rc = futex_wake_op(1, 1, encode(op, 0, 0x111, 0x111)); + if (rc != -ENOSYS) { + FAIL("an unimplemented op must be ENOSYS"); + return; + } + if (__atomic_load_n(&target_word, __ATOMIC_ACQUIRE) != 0) { + FAIL("a refused op must not have modified the word"); + return; + } + PASS(); +} + +static void unsupported_cmp_case(const char *name, unsigned cmp) +{ + TEST(name); + __atomic_store_n(&target_word, 0, __ATOMIC_RELEASE); + long rc = futex_wake_op(1, 1, encode(0, cmp, 0x111, 0x111)); + if (rc != -ENOSYS) { + FAIL("an unimplemented comparison must be ENOSYS"); + return; + } + + /* The comparison is refused after the modify, so unlike the op case the + * word carries the operand. + */ + if (__atomic_load_n(&target_word, __ATOMIC_ACQUIRE) != 0x111) { + FAIL("a refused comparison must still have modified the word"); + return; + } + PASS(); +} + +int main(void) +{ + /* CLONE_VM | CLONE_FS | CLONE_FILES | CLONE_SIGHAND | CLONE_THREAD | + * CLONE_SYSVSEM, spelled as the value the way the sibling futex tests do. + */ + unsigned long flags = 0x50f00; + + printf("=== futex wake_op selector tests ===\n\n"); + + TEST("a supported pair modifies the word"); + __atomic_store_n(&target_word, 0, __ATOMIC_RELEASE); + long rc = futex_wake_op(1, 1, valid_val3()); + if (rc < 0) { + FAIL("a supported op and comparison must not be refused"); + } else if (__atomic_load_n(&target_word, __ATOMIC_ACQUIRE) != 0x111) { + FAIL("a supported op must have modified the word"); + } else { + PASS(); + } + + unsupported_op_case("op 5 is ENOSYS", 5); + unsupported_op_case("op 6 is ENOSYS", 6); + unsupported_op_case("op 7 is ENOSYS", 7); + + unsupported_cmp_case("comparison 6 is ENOSYS", 6); + unsupported_cmp_case("comparison 15 is ENOSYS", 15); + + /* Both unassigned: the op is read first, so the word stays untouched. */ + unsupported_op_case("an unsupported pair stops at the op", 5); + + TEST("clone the waiter"); + long waiter = raw_clone(flags, waiter_stack + 16384, 0, 0, 0); + if (waiter == 0) { + waiter_fn(); + __builtin_unreachable(); + } + if (waiter < 0) { + FAIL("waiter clone failed"); + goto done; + } + PASS(); + + while (__atomic_load_n(&waiter_parking, __ATOMIC_ACQUIRE) == 0) + raw_futex_wait(&waiter_parking, 0); + settle(); + + TEST("a refused op leaves the waiter parked"); + if (futex_wake_op(1, 1, encode(5, 0, 0x111, 0x111)) != -ENOSYS) { + FAIL("an unimplemented op must be ENOSYS"); + goto release; + } + settle(); + if (!parked()) { + FAIL("a refused op woke a parked waiter"); + goto release; + } + PASS(); + + TEST("a refused comparison leaves the waiter parked"); + if (futex_wake_op(1, 1, encode(0, 6, 0x111, 0x111)) != -ENOSYS) { + FAIL("an unimplemented comparison must be ENOSYS"); + goto release; + } + settle(); + if (!parked()) { + FAIL("a refused comparison woke a parked waiter"); + goto release; + } + PASS(); + + /* The waiter is still there, so a supported pair reaches it. This is also + * what keeps the two cases above from passing on a waiter that never + * parked: one that had gone leaves nothing to wake here. + */ + TEST("a supported op wakes the waiter left behind"); + __atomic_store_n(&park_word, 1, __ATOMIC_RELEASE); + if (futex_wake_op(1, 1, valid_val3()) != 1) { + FAIL("the waiter the refused calls left parked was not woken"); + goto release; + } + PASS(); + +release: + __atomic_store_n(&park_word, 1, __ATOMIC_RELEASE); + while (__atomic_load_n(&waiter_done, __ATOMIC_ACQUIRE) == 0) { + raw_futex_wake(&park_word, 1); + raw_syscall0(__NR_sched_yield); + } + +done: + SUMMARY("test-futex-wake-op-enosys"); + return fails > 0 ? 1 : 0; +} diff --git a/tests/test-matrix.sh b/tests/test-matrix.sh index d9970e27..1ae28a6b 100755 --- a/tests/test-matrix.sh +++ b/tests/test-matrix.sh @@ -894,6 +894,8 @@ run_unit_tests() "$bindir/test-futex-requeue-account" test_rc "$runner" "test-futex-requeue-pi" 0 \ "$bindir/test-futex-requeue-pi" + test_rc "$runner" "test-futex-wake-op-enosys" 0 \ + "$bindir/test-futex-wake-op-enosys" test_rc "$runner" "test-robust-futex" 0 "$bindir/test-robust-futex" test_check "$runner" "test-shim-futex-fast" "OK" \ "$bindir/test-shim-futex-fast" From d7f45d14053980ea71a08adb6831343b2f90a743 Mon Sep 17 00:00:00 2001 From: alanhc Date: Wed, 2 Sep 2026 22:06:11 +0800 Subject: [PATCH 05/11] Make the futexwakeop gate bite "PROVED 92 of 92" says nothing about whether the clauses are load bearing, so give the new target the four mutations check-mutants.py wants: accept every op, accept every comparison selector, drop the complement from ANDN so it becomes AND, and widen LT to LE. All four are caught. The first two are the ENOSYS gates themselves; the other two sit inside a switch arm, which is where a postcondition that pinned only a range rather than a value would have let a wrong answer through. --- scripts/check-mutants.py | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 0e4c08c9..26b96d19 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -196,6 +196,39 @@ def _load(stem, name): " return (uint64_t) nr_wake + nr_requeue;\n", " return (uint64_t) nr_requeue;\n", ), + # ---- verify-futexwakeop ------------------------------------------------ + ( + "futexwakeop", + "src/proved/futexwakeop.h", + "futex_wake_op_supported", + "accept every op (an unassigned encoding stops being ENOSYS)", + " return op <= FUTEX_WAKE_OP_MAX;\n", + " return 1;\n", + ), + ( + "futexwakeop", + "src/proved/futexwakeop.h", + "futex_wake_cmp_supported", + "accept every comparison selector", + " return cmp <= FUTEX_WAKE_CMP_MAX;\n", + " return 1;\n", + ), + ( + "futexwakeop", + "src/proved/futexwakeop.h", + "futex_wake_op_apply", + "drop the complement from ANDN (it becomes AND)", + " return old_val & ~op_val;\n", + " return old_val & op_val;\n", + ), + ( + "futexwakeop", + "src/proved/futexwakeop.h", + "futex_wake_op_cmp", + "widen LT to LE (the boundary case flips)", + " return old_val < cmp_arg;\n", + " return old_val <= cmp_arg;\n", + ), # ---- verify-futexop ---------------------------------------------------- ( "futexop", From f807377a404b526984d335dd9fd5a99e10cff4da Mon Sep 17 00:00:00 2001 From: Hung-Chun Tseng Date: Thu, 3 Sep 2026 00:36:34 +0800 Subject: [PATCH 06/11] Wake both readers of holder_ready Two threads wait on holder_ready, main and the waiter, and the holder sets it once. set_and_wake wakes one, so whichever reader was already parked when the other was woken stays parked: the flag never returns to zero, and nothing sets it a second time. The run then hangs in wait_until_set until the harness kills it. Both readers normally observe the store before they reach FUTEX_WAIT, which is why this survived every local run. Those hosts have hardware virtualization, so the window between the load in wait_until_set and the wait behind it is narrow. The matrix's qemu-aarch64 lane has no such acceleration on a CI runner -- macOS gives a guest no nested virtualization, so qemu falls back to tcg -- and the window is wide enough there to lose. Measured under QEMU_ACCEL=tcg on Linux 6.18.44, the lane hung about one run in three; with this change it passed 20 of 20. The lane's own failure was a timeout with no output, which named nothing. Only holder_ready takes the all-waiters wake. The other three flags have exactly one reader each, and leaving them on set_and_wake is what keeps that visible. --- tests/test-futex-requeue-pi.c | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/tests/test-futex-requeue-pi.c b/tests/test-futex-requeue-pi.c index 83b62cf1..d6628859 100644 --- a/tests/test-futex-requeue-pi.c +++ b/tests/test-futex-requeue-pi.c @@ -17,6 +17,7 @@ * Syscalls exercised: futex(98), clone(220), gettid(178), exit(93), sched_yield */ +#include #include #include #include @@ -70,6 +71,25 @@ static void set_and_wake(int *addr) raw_futex_wake(addr, 1); } +/* holder_ready is the one flag two threads wait on, main and the waiter, and it + * is set once. Waking a single one of them strands the other for good, because + * the flag never returns to zero and no second wake is coming. + * + * Both readers usually observe the store before they park, which is why the + * single wake survived every run on a host with hardware virtualization. Under + * qemu's tcg the window between the load in wait_until_set and the FUTEX_WAIT + * behind it is wide enough to lose, and the matrix's qemu-aarch64 lane hung + * there about one run in three. + * + * The other three flags keep set_and_wake. Each has exactly one reader, and + * leaving them alone is what keeps that readable. + */ +static void set_and_wake_all(int *addr) +{ + __atomic_store_n(addr, 1, __ATOMIC_RELEASE); + raw_futex_wake(addr, INT_MAX); +} + static void wait_until_set(int *addr) { while (__atomic_load_n(addr, __ATOMIC_ACQUIRE) == 0) @@ -82,7 +102,7 @@ static void wait_until_set(int *addr) static void holder_fn(void) { if (futex_lock_pi(&pi_lock) == 0) { - set_and_wake(&holder_ready); + set_and_wake_all(&holder_ready); wait_until_set(&release); futex_unlock_pi(&pi_lock); } else { @@ -90,7 +110,7 @@ static void holder_fn(void) * whose LOCK_PI is broken is the one this lane exists to catch. */ set_and_wake(&holder_failed); - set_and_wake(&holder_ready); + set_and_wake_all(&holder_ready); } raw_exit(0); } From be8be9895397c13239643be6e001c169214d5eab Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 00:42:39 +0800 Subject: [PATCH 07/11] Prove the PI lock word transitions The PI word carries three fields a guest can write any bit pattern into: the owner TID in bits 0-29, FUTEX_OWNER_DIED in bit 30, FUTEX_WAITERS in bit 31. Reading and editing them was open-coded at seventeen sites across futex_lock_pi_inner, futex_unlock_pi, the WAITERS-clear helper and robust_list_walk, with the death transition written out twice. src/proved/futexpi.h collects them behind seven functions and WP discharges 38 obligations over the lot. The one worth a contract rather than a mask is the death transition: it has to clear the TID, set OWNER_DIED and leave WAITERS alone, and the three postconditions pin every bit of the answer. A walk that dropped the waiters bit leaves a lock nobody is ever woken from, which no test in the tree would have caught. The waiters bit is read as a magnitude and edited as a remainder rather than with the bit operators. Under the bitwise spelling the "leaves the rest alone" clause on set_waiters times out at 30s on both provers, while every other clause in the file discharges in seconds; futexop.h documents the same wall and takes the same way around it. Nothing about the shipped code needs the operators. The transition is now spelled the way handle_futex_death() spells it, (uval & FUTEX_WAITERS) | FUTEX_OWNER_DIED, rather than as a TID clear. The two agree on every input, since the OR sets bit 30 whatever the mask left there, and the kernel's form is the one a reader can check against the reference. Checked against that reference rather than assumed: on Linux 6.18.44 through the qemu lane, a robust owner's death leaves 0x40000000 on an uncontended word and 0xC0000000 on one that already had waiters. elfuse answers the same for both, before and after this commit. test-robust-futex asserted only that OWNER_DIED was set, so neither of the other two fields had coverage. It now puts a case to each, including the contended word, and passes unchanged on the reference kernel. --- mk/verify.mk | 11 ++++ src/proved/futexpi.h | 107 ++++++++++++++++++++++++++++++++++++++ src/runtime/futex.c | 50 +++++++----------- tests/test-robust-futex.c | 95 +++++++++++++++++++++------------ 4 files changed, 201 insertions(+), 62 deletions(-) create mode 100644 src/proved/futexpi.h diff --git a/mk/verify.mk b/mk/verify.mk index fd61828d..1ba01dfb 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -410,6 +410,17 @@ VERIFY_FUTEXWAKEOP_SCAN := src/proved/futexwakeop.h VERIFY_FUTEXWAKEOP_CLAIM := for ANY guest-supplied op and comparison selector VERIFY_FUTEXWAKEOP_UNPROVED := the wake walks the selectors gate stay test-covered +VERIFY_FUTEXPI_SRC := src/proved/futexpi.h +VERIFY_FUTEXPI_FCTS := futex_pi_owner_tid futex_pi_unowned futex_pi_owner_died \ + futex_pi_has_waiters futex_pi_set_waiters \ + futex_pi_clear_waiters futex_pi_mark_owner_died +VERIFY_FUTEXPI_MIN_GOALS ?= 38 +# typed: one scalar in, one scalar out, no buffer and no aliasing question. +VERIFY_FUTEXPI_MODEL := typed +VERIFY_FUTEXPI_SCAN := src/proved/futexpi.h +VERIFY_FUTEXPI_CLAIM := for ANY bit pattern a guest can write to a PI lock word +VERIFY_FUTEXPI_UNPROVED := the CAS loops around them stay test-covered + VERIFY_PATHDEPTH_SRC := src/proved/pathdepth.h VERIFY_PATHDEPTH_FCTS := path_depth_push path_depth_pop VERIFY_PATHDEPTH_MIN_GOALS ?= 24 diff --git a/src/proved/futexpi.h b/src/proved/futexpi.h new file mode 100644 index 00000000..7666e175 --- /dev/null +++ b/src/proved/futexpi.h @@ -0,0 +1,107 @@ +/* + * The PI lock word, split out of the FUTEX_LOCK_PI paths and robust_list_walk + * in src/runtime/futex.c and proved here. + * + * Layout, which Linux fixes and a guest can write any bit pattern into: + * + * bits 0-29 owner TID (FUTEX_TID_MASK) + * bit 30 FUTEX_OWNER_DIED + * bit 31 FUTEX_WAITERS + * + * The death transition is the one worth a contract rather than a mask: it has + * to clear the TID, set OWNER_DIED and leave WAITERS alone, and an owner whose + * waiters bit it dropped is a lock nobody is ever woken from. + */ +#pragma once + +#include + +#define FUTEX_PI_TID_MASK 0x3FFFFFFFu +#define FUTEX_PI_OWNER_DIED 0x40000000u +#define FUTEX_PI_WAITERS 0x80000000u + +/*@ + assigns \nothing; + ensures bounded: \result <= 0x3FFFFFFF; + ensures exact: \result == (word & 0x3FFFFFFF); + */ +static inline uint32_t futex_pi_owner_tid(uint32_t word) +{ + return word & FUTEX_PI_TID_MASK; +} + +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: \result != 0 <==> (word & 0x3FFFFFFF) == 0; + */ +static inline int futex_pi_unowned(uint32_t word) +{ + return (word & FUTEX_PI_TID_MASK) == 0; +} + +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: \result != 0 <==> (word & 0x40000000) != 0; + */ +static inline int futex_pi_owner_died(uint32_t word) +{ + return (word & FUTEX_PI_OWNER_DIED) != 0; +} + +/* WAITERS is the top bit, so the three below read it as magnitude and edit it + * as a remainder. Under the bitwise spelling the "leaves the rest alone" + * clauses time out at 30s on both provers, the wall futexop.h documents; these + * forms discharge. Nothing about the shipped code needs the bit operators. + */ +/*@ + assigns \nothing; + ensures binary: \result == 0 || \result == 1; + ensures exact: \result != 0 <==> word >= 0x80000000; + */ +static inline int futex_pi_has_waiters(uint32_t word) +{ + return word >= FUTEX_PI_WAITERS; +} + +/* The two edits a waiter makes to the flag, neither of which may disturb the + * owner field between them. + */ +/*@ + assigns \nothing; + ensures set: \result >= 0x80000000; + ensures others_kept: \result % 0x80000000 == word % 0x80000000; + */ +static inline uint32_t futex_pi_set_waiters(uint32_t word) +{ + return word % FUTEX_PI_WAITERS + FUTEX_PI_WAITERS; +} + +/*@ + assigns \nothing; + ensures clear: \result < 0x80000000; + ensures others_kept: \result % 0x80000000 == word % 0x80000000; + */ +static inline uint32_t futex_pi_clear_waiters(uint32_t word) +{ + return word % FUTEX_PI_WAITERS; +} + +/* What robust_list_walk writes over a lock whose owner exited holding it. + * + * Spelled the way handle_futex_death() in kernel/futex/core.c spells it. The + * three postconditions pin every bit of the answer: the low 30 are zero, bit 30 + * is set, bit 31 is whatever it was. + */ +/*@ + assigns \nothing; + ensures tid_cleared: (\result & 0x3FFFFFFF) == 0; + ensures died_set: (\result & 0x40000000) != 0; + ensures waiters_kept: \result >= 0x80000000 <==> word >= 0x80000000; + */ +static inline uint32_t futex_pi_mark_owner_died(uint32_t word) +{ + return (word >= FUTEX_PI_WAITERS ? FUTEX_PI_WAITERS : 0u) | + FUTEX_PI_OWNER_DIED; +} diff --git a/src/runtime/futex.c b/src/runtime/futex.c index 6f156e7d..12c0499f 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -42,6 +42,7 @@ #include "debug/log.h" #include "proved/futexhash.h" #include "proved/futexop.h" +#include "proved/futexpi.h" #include "proved/futexreq.h" #include "proved/futexwakeop.h" #include "proved/timespec.h" @@ -108,18 +109,9 @@ _Static_assert(FUTEX_WAKE_BITSET == 10, #define FUTEX_BITSET_MATCH_ANY 0xFFFFFFFFU -/* PI futex word layout (bits): - * 0-29: TID of lock holder (0 = unlocked) - * 30: FUTEX_OWNER_DIED (set by robust_list_walk on thread exit) - * 31: FUTEX_WAITERS (at least one thread is blocked) - * - * Linux kernel: FUTEX_WAITERS=0x80000000 (bit 31), FUTEX_OWNER_DIED=0x40000000 - * (bit 30), FUTEX_TID_MASK=0x3FFFFFFF. FUTEX_OWNER_DIED=0x40000000 (bit 30) is - * set by robust_list_walk on thread exit. FUTEX_TID_MASK is 30 bits. +/* The PI word's three fields and the edits made to them are proved/futexpi.h, + * which carries the layout and Linux's own constants. */ -#define FUTEX_TID_MASK 0x3FFFFFFFU -#define FUTEX_OWNER_DIED 0x40000000U -#define FUTEX_WAITERS 0x80000000U /* Address-wait helper state. * @@ -521,9 +513,9 @@ static void futex_clear_waiters_bit(uint32_t *word) bool cleared; if (!futex_word_load(word, &v)) return; - if (!(v & FUTEX_WAITERS)) + if (!futex_pi_has_waiters(v)) return; - if (!futex_word_cas(word, &v, v & ~FUTEX_WAITERS, &cleared)) + if (!futex_word_cas(word, &v, futex_pi_clear_waiters(v), &cleared)) return; if (cleared) return; @@ -1766,7 +1758,7 @@ static int64_t futex_lock_pi_inner(guest_t *g, return 0; /* Already own it? Deadlock (Linux returns EDEADLK) */ - if ((expected & FUTEX_TID_MASK) == tid) + if (futex_pi_owner_tid(expected) == tid) return -LINUX_EDEADLK; /* Robust owner death: the robust-list walk sets FUTEX_OWNER_DIED and @@ -1777,7 +1769,7 @@ static int64_t futex_lock_pi_inner(guest_t *g, * which never sees a robust-cleaned word (TID == 0) and would otherwise * spin forever. */ - if (expected & FUTEX_OWNER_DIED) { + if (futex_pi_owner_died(expected)) { if (!futex_word_cas(word, &expected, 0, NULL)) return -LINUX_EFAULT; continue; /* Retry acquisition */ @@ -1788,7 +1780,7 @@ static int64_t futex_lock_pi_inner(guest_t *g, * FUTEX_LOCK_PI returns -ESRCH (attach_to_pi_owner -> * handle_exit_race). */ - uint32_t owner_tid = expected & FUTEX_TID_MASK; + uint32_t owner_tid = futex_pi_owner_tid(expected); if (owner_tid != 0 && !thread_find((int64_t) owner_tid)) return -LINUX_ESRCH; @@ -1800,11 +1792,11 @@ static int64_t futex_lock_pi_inner(guest_t *g, uint32_t cur; if (!futex_word_load(word, &cur)) return -LINUX_EFAULT; - if ((cur & FUTEX_TID_MASK) == 0) + if (futex_pi_unowned(cur)) break; /* Owner released; retry outer loop */ - if (cur & FUTEX_WAITERS) + if (futex_pi_has_waiters(cur)) break; /* Already set by another waiter */ - uint32_t desired = cur | FUTEX_WAITERS; + uint32_t desired = futex_pi_set_waiters(cur); bool marked; if (!futex_word_cas(word, &cur, desired, &marked)) return -LINUX_EFAULT; @@ -1816,7 +1808,7 @@ static int64_t futex_lock_pi_inner(guest_t *g, uint32_t cur; if (!futex_word_load(word, &cur)) return -LINUX_EFAULT; - if ((cur & FUTEX_TID_MASK) == 0) + if (futex_pi_unowned(cur)) continue; /* Enqueue and block */ @@ -1829,7 +1821,7 @@ static int64_t futex_lock_pi_inner(guest_t *g, pthread_mutex_unlock(&b->lock); return -LINUX_EFAULT; } - if ((cur & FUTEX_TID_MASK) == 0) { + if (futex_pi_unowned(cur)) { pthread_mutex_unlock(&b->lock); continue; } @@ -1976,11 +1968,11 @@ static int64_t futex_lock_pi_inner(guest_t *g, pthread_cond_destroy(&waiter.cond); return -LINUX_EFAULT; } - if (check & FUTEX_OWNER_DIED) { + if (futex_pi_owner_died(check)) { owner_died = true; break; } - uint32_t check_tid = check & FUTEX_TID_MASK; + uint32_t check_tid = futex_pi_owner_tid(check); if (check_tid != 0 && !thread_tid_alive((int64_t) check_tid)) { bucket_unlink_locked(b, &waiter); pthread_mutex_unlock(&b->lock); @@ -2074,7 +2066,7 @@ static int64_t futex_unlock_pi(guest_t *g, uint64_t uaddr) uint32_t cur; if (guest_read_small(g, uaddr, &cur, sizeof(cur)) != 0) return -LINUX_EFAULT; - if ((cur & FUTEX_TID_MASK) != tid) + if (futex_pi_owner_tid(cur) != tid) return -LINUX_EPERM; /* Only the owner reaches here, and an owned PI lock is always aligned @@ -2629,11 +2621,10 @@ void robust_list_walk(guest_t *g, thread_entry_t *t) if (guest_read_small(g, futex_gva, &futex_val, sizeof(futex_val)) == 0) { /* Only act if this thread owns the lock */ - uint32_t owner = futex_val & FUTEX_TID_MASK; + uint32_t owner = futex_pi_owner_tid(futex_val); if (owner == (uint32_t) thread_tid(t)) { /* Set FUTEX_OWNER_DIED and clear TID */ - uint32_t new_val = - (futex_val & ~FUTEX_TID_MASK) | FUTEX_OWNER_DIED; + uint32_t new_val = futex_pi_mark_owner_died(futex_val); if (guest_write_small(g, futex_gva, &new_val, sizeof(new_val)) < 0) log_debug( @@ -2673,10 +2664,9 @@ void robust_list_walk(guest_t *g, thread_entry_t *t) uint32_t futex_val; if (guest_read_small(g, futex_gva, &futex_val, sizeof(futex_val)) == 0) { - uint32_t owner = futex_val & FUTEX_TID_MASK; + uint32_t owner = futex_pi_owner_tid(futex_val); if (owner == (uint32_t) thread_tid(t)) { - uint32_t new_val = - (futex_val & ~FUTEX_TID_MASK) | FUTEX_OWNER_DIED; + uint32_t new_val = futex_pi_mark_owner_died(futex_val); if (guest_write_small(g, futex_gva, &new_val, sizeof(new_val)) < 0) log_debug( diff --git a/tests/test-robust-futex.c b/tests/test-robust-futex.c index 72050bce..e99b0ec2 100644 --- a/tests/test-robust-futex.c +++ b/tests/test-robust-futex.c @@ -51,6 +51,7 @@ static struct robust_list_head rhead __attribute__((aligned(8))); static struct robust_list entry1 __attribute__((aligned(8))); static char child_stack[8192] __attribute__((aligned(16))); +static volatile int preset_waiters; static int child_fn(void *arg) { @@ -63,8 +64,11 @@ static int child_fn(void *arg) rhead.list_op_pending = NULL; entry1.next = &rhead.list; /* circular: points back to head */ - /* "Acquire" the lock by writing the current TID */ - lock_word = (uint32_t) tid; + /* "Acquire" the lock by writing the current TID, with WAITERS already set + * when the case under test wants it there. + */ + lock_word = + (uint32_t) tid | (preset_waiters ? (uint32_t) FUTEX_WAITERS : 0u); /* Register robust list with kernel */ raw_syscall2(99, (long) &rhead, sizeof(rhead)); /* set_robust_list */ @@ -76,48 +80,75 @@ static int child_fn(void *arg) test_unreachable(); } -int main(void) +/* One owner-dies run. + * + * Returns the word the robust walk left behind, or 0 with *ok cleared if the + * thread could not be started. + */ +static uint32_t run_owner_death(int waiters, int *ok) { - TEST("robust-futex: owner-died on exit"); - + *ok = 1; lock_word = 0; memset(&rhead, 0, sizeof(rhead)); memset(&entry1, 0, sizeof(entry1)); + preset_waiters = waiters; - /* Clone a thread: CLONE_THREAD | CLONE_VM | CLONE_FS | CLONE_SIGHAND | + /* CLONE_THREAD | CLONE_VM | CLONE_FS | CLONE_SIGHAND | * CLONE_CHILD_CLEARTID. CLONE_THREAD implies CLONE_VM and CLONE_SIGHAND. */ - long flags = 0x00010000 /* CLONE_THREAD */ - | 0x00000100 /* CLONE_VM */ - | 0x00000200 /* CLONE_FS */ - | 0x00000800 /* CLONE_SIGHAND */ - | 0x00200000; /* CLONE_CHILD_CLEARTID */ + long flags = 0x00010000 | 0x00000100 | 0x00000200 | 0x00000800 | 0x00200000; - /* Use raw_syscall5 for clone(flags, stack, ptid, tls, ctid) */ volatile int child_tid_addr = 0; - long ret = raw_syscall5(220, /* clone */ - flags, (long) (child_stack + sizeof(child_stack)), - 0, /* parent_tid */ - 0, /* tls */ - (long) &child_tid_addr /* child_tid */ - ); - + long ret = + raw_syscall5(220, flags, (long) (child_stack + sizeof(child_stack)), 0, + 0, (long) &child_tid_addr); + if (ret == 0) { + child_fn(NULL); + test_unreachable(); + } if (ret < 0) { + *ok = 0; + return 0; + } + usleep(100000); /* grace period for the exit-time walk */ + return lock_word; +} + +int main(void) +{ + int ok; + + TEST("robust-futex: owner-died on exit"); + uint32_t plain = run_owner_death(0, &ok); + if (!ok) { + FAIL("clone failed"); + } else { + EXPECT_TRUE(plain & FUTEX_OWNER_DIED, "FUTEX_OWNER_DIED not set"); + } + + /* The walk owes the word two more things than the flag. A TID left behind + * is an owner no LOCK_PI can displace, and it is what separates the robust + * path from an ordinary abandoned lock. + */ + TEST("robust-futex: owner-died clears the TID"); + EXPECT_TRUE(ok && (plain & FUTEX_TID_MASK) == 0, + "the dead owner's TID survived the walk"); + + TEST("robust-futex: owner-died keeps WAITERS clear"); + EXPECT_TRUE(ok && (plain & FUTEX_WAITERS) == 0, + "WAITERS appeared on a word that never had it"); + + /* Same transition over a word that already had waiters: the bit has to + * survive, or the parked waiter is never woken. + */ + TEST("robust-futex: owner-died keeps WAITERS set"); + uint32_t contended = run_owner_death(1, &ok); + if (!ok) { FAIL("clone failed"); - } else if (ret == 0) { - /* Child */ - child_fn(NULL); } else { - /* Parent: wait for child to exit via CLONE_CHILD_CLEARTID futex */ - usleep(100000); /* 100ms grace period */ - - /* Check if FUTEX_OWNER_DIED was set */ - uint32_t val = lock_word; - if (val & FUTEX_OWNER_DIED) { - PASS(); - } else { - FAIL("FUTEX_OWNER_DIED not set"); - } + EXPECT_TRUE(contended == ((uint32_t) FUTEX_WAITERS | + (uint32_t) FUTEX_OWNER_DIED), + "a contended lock's word is not WAITERS|OWNER_DIED"); } TEST("robust-futex: set_robust_list returns 0"); From ead5f576271830d33c7612adc54203e1e98f9236 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 00:42:52 +0800 Subject: [PATCH 08/11] Make the futexpi gate bite Seven mutations, one per proved function, so no clause in the file is carried without evidence that it rejects something: read the flag bits as part of the TID, call a word unowned whenever any bit is clear, read the waiters bit as the death flag, move the has_waiters boundary by one, clear OWNER_DIED along with WAITERS, drop the remainder from set_waiters, and drop the waiters bit from the death transition. All seven are caught. The set_waiters one is the reason that function takes a remainder before it adds: without it a word that already had the bit carries past bit 31 and loses it. That input is unreachable from the one call site today, which breaks on futex_pi_has_waiters before it gets there. The contract is still stated over every word, because the guard and the edit are separate lines and only one of them is what makes the answer right. --- scripts/check-mutants.py | 57 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 26b96d19..a2eb0fe5 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -196,6 +196,63 @@ def _load(stem, name): " return (uint64_t) nr_wake + nr_requeue;\n", " return (uint64_t) nr_requeue;\n", ), + # ---- verify-futexpi ---------------------------------------------------- + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_owner_tid", + "read the flag bits as part of the TID", + " return word & FUTEX_PI_TID_MASK;\n", + " return word;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_set_waiters", + "drop the remainder (a word that already had the bit doubles it away)", + " return word % FUTEX_PI_WAITERS + FUTEX_PI_WAITERS;\n", + " return word + FUTEX_PI_WAITERS;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_mark_owner_died", + "drop the waiters bit from the death transition", + " return (word >= FUTEX_PI_WAITERS ? FUTEX_PI_WAITERS : 0u) |\n FUTEX_PI_OWNER_DIED;\n", + " return FUTEX_PI_OWNER_DIED;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_unowned", + "call a word unowned whenever any bit is clear", + " return (word & FUTEX_PI_TID_MASK) == 0;\n", + " return word != 0xFFFFFFFFu;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_owner_died", + "read the waiters bit as the death flag", + " return (word & FUTEX_PI_OWNER_DIED) != 0;\n", + " return (word & FUTEX_PI_WAITERS) != 0;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_has_waiters", + "off by one at the boundary word", + " return word >= FUTEX_PI_WAITERS;\n", + " return word > FUTEX_PI_WAITERS;\n", + ), + ( + "futexpi", + "src/proved/futexpi.h", + "futex_pi_clear_waiters", + "clear the death flag along with the waiters bit", + " return word % FUTEX_PI_WAITERS;\n", + " return word % FUTEX_PI_OWNER_DIED;\n", + ), # ---- verify-futexwakeop ------------------------------------------------ ( "futexwakeop", From 4808451387b1f2f86a41a6863381386fda317455 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 08:40:17 +0800 Subject: [PATCH 09/11] Prove the robust walk ran before reading the word The owner-died cases waited for the exiting thread with a fixed 100ms usleep, then asserted on the word the robust walk was supposed to have rewritten. A sleep is a guess about the walk, not a proof of it: on a loaded machine the assertions read a word the walk had not reached yet. The clone+exit cycle now runs twice over one static child stack, so the second run also needs the first child to be off that stack before it starts. The exit path already publishes exactly the fact the test needs. robust_list_walk runs immediately before the CLONE_CHILD_CLEARTID store in the worker teardown, so a cleared ctid word is proof the walk finished. Wait on it with plain FUTEX_WAIT, matching the wake that CLEARTID issues, and bound the wait so a stuck teardown is a reported failure rather than a driver timeout. The word only carries that proof once something seeds it. The clone flags asked for CLONE_CHILD_CLEARTID but not CLONE_PARENT_SETTID, which left the address zero from the start, so a futex wait on it would have returned at once and waited for nothing. Pass the address as ptid too, as test-thread and test-futex-pi already do. Setup failures also reported three times: the two follow-up assertions folded ok into the condition, so a failed clone produced FAILs about a surviving TID and an appearing WAITERS bit on top of the real message. Carry the reason as a string instead, which also keeps a join timeout from being reported as a clone failure, and skip the dependent checks when the run never produced a word. --- tests/test-robust-futex.c | 83 ++++++++++++++++++++++++++------------- 1 file changed, 56 insertions(+), 27 deletions(-) diff --git a/tests/test-robust-futex.c b/tests/test-robust-futex.c index e99b0ec2..0f9890b9 100644 --- a/tests/test-robust-futex.c +++ b/tests/test-robust-futex.c @@ -15,7 +15,7 @@ #include #include -#include +#include #include #include "test-harness.h" @@ -80,71 +80,100 @@ static int child_fn(void *arg) test_unreachable(); } +/* Wait for a cloned thread to finish tearing down. CLEARTID zeroes the address + * only after the robust walk has run, so a cleared word proves the walk + * finished and the reused child stack is free. -1 if it never clears. + */ +static int join_child(volatile int *ctid) +{ + /* Plain FUTEX_WAIT: the CLEARTID wake is not private. The timeout only + * turns a stuck teardown into a reported failure. + */ + struct timespec ts = {.tv_sec = 1, .tv_nsec = 0}; + + for (int i = 0; i < 10; i++) { + int seen = __atomic_load_n(ctid, __ATOMIC_SEQ_CST); + if (seen == 0) + return 0; + raw_syscall6(98, (long) ctid, FUTEX_WAIT, seen, (long) &ts, 0, 0); + } + return __atomic_load_n(ctid, __ATOMIC_SEQ_CST) == 0 ? 0 : -1; +} + /* One owner-dies run. * - * Returns the word the robust walk left behind, or 0 with *ok cleared if the - * thread could not be started. + * Returns the word the robust walk left behind; on failure *err names what went + * wrong and the word means nothing. */ -static uint32_t run_owner_death(int waiters, int *ok) +static uint32_t run_owner_death(int waiters, const char **err) { - *ok = 1; + *err = NULL; lock_word = 0; memset(&rhead, 0, sizeof(rhead)); memset(&entry1, 0, sizeof(entry1)); preset_waiters = waiters; - /* CLONE_THREAD | CLONE_VM | CLONE_FS | CLONE_SIGHAND | - * CLONE_CHILD_CLEARTID. CLONE_THREAD implies CLONE_VM and CLONE_SIGHAND. + /* CLONE_THREAD | CLONE_VM | CLONE_FS | CLONE_SIGHAND | CLONE_PARENT_SETTID + * | CLONE_CHILD_CLEARTID. CLONE_THREAD implies CLONE_VM and CLONE_SIGHAND. + * PARENT_SETTID seeds the word CLEARTID later zeroes, so join_child has + * something to wait on. */ - long flags = 0x00010000 | 0x00000100 | 0x00000200 | 0x00000800 | 0x00200000; + long flags = 0x00010000 | 0x00000100 | 0x00000200 | 0x00000800 | + 0x00100000 | 0x00200000; volatile int child_tid_addr = 0; long ret = - raw_syscall5(220, flags, (long) (child_stack + sizeof(child_stack)), 0, - 0, (long) &child_tid_addr); + raw_syscall5(220, flags, (long) (child_stack + sizeof(child_stack)), + (long) &child_tid_addr, 0, (long) &child_tid_addr); if (ret == 0) { child_fn(NULL); test_unreachable(); } if (ret < 0) { - *ok = 0; + *err = "clone failed"; + return 0; + } + if (join_child(&child_tid_addr) != 0) { + *err = "child never cleared its CLEARTID word"; return 0; } - usleep(100000); /* grace period for the exit-time walk */ return lock_word; } int main(void) { - int ok; + const char *err; TEST("robust-futex: owner-died on exit"); - uint32_t plain = run_owner_death(0, &ok); - if (!ok) { - FAIL("clone failed"); + uint32_t plain = run_owner_death(0, &err); + if (err) { + FAIL(err); } else { EXPECT_TRUE(plain & FUTEX_OWNER_DIED, "FUTEX_OWNER_DIED not set"); } /* The walk owes the word two more things than the flag. A TID left behind * is an owner no LOCK_PI can displace, and it is what separates the robust - * path from an ordinary abandoned lock. + * path from an ordinary abandoned lock. A run that never started says + * nothing about either, so it reports once above. */ - TEST("robust-futex: owner-died clears the TID"); - EXPECT_TRUE(ok && (plain & FUTEX_TID_MASK) == 0, - "the dead owner's TID survived the walk"); - - TEST("robust-futex: owner-died keeps WAITERS clear"); - EXPECT_TRUE(ok && (plain & FUTEX_WAITERS) == 0, - "WAITERS appeared on a word that never had it"); + if (!err) { + TEST("robust-futex: owner-died clears the TID"); + EXPECT_TRUE((plain & FUTEX_TID_MASK) == 0, + "the dead owner's TID survived the walk"); + + TEST("robust-futex: owner-died keeps WAITERS clear"); + EXPECT_TRUE((plain & FUTEX_WAITERS) == 0, + "WAITERS appeared on a word that never had it"); + } /* Same transition over a word that already had waiters: the bit has to * survive, or the parked waiter is never woken. */ TEST("robust-futex: owner-died keeps WAITERS set"); - uint32_t contended = run_owner_death(1, &ok); - if (!ok) { - FAIL("clone failed"); + uint32_t contended = run_owner_death(1, &err); + if (err) { + FAIL(err); } else { EXPECT_TRUE(contended == ((uint32_t) FUTEX_WAITERS | (uint32_t) FUTEX_OWNER_DIED), From 84b47c37f5e15d8d6d06c0e83e803a9dfbe33ab6 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:06:33 +0800 Subject: [PATCH 10/11] Prove the bucket set a futex_waitv locks sys_futex_waitv takes up to 128 guest-chosen addresses, hashes each to one of 1024 buckets, and locks the distinct buckets in ascending index order, releasing them in reverse. Two entries hashing alike is ordinary rather than exceptional: the guest picks the addresses. What holds the call together is that the bucket set comes out sorted and without repeats. A repeat locks one non-recursive mutex twice, which is a hang and not an errno. An unsorted set takes the bucket locks out of the order every other futex path takes them in. Both properties lived in an open-coded insertion sort with no contract and no test. src/proved/futexwaitv.h states them as postconditions on the insertion and WP discharges 36 obligations: the answer grows by at most one, stays strictly sorted, contains the index just offered, and is longer exactly when that index was absent. The parallel bucket_ptrs array is gone. Every entry in it was &buckets[bucket_ids[i]], so it carried no information, and shifting two arrays in lockstep is what the proved insertion would have had to replicate. The three lock sites index buckets directly now. Checked before the contract was written rather than after: on the reference kernel and on elfuse alike, a wait set holding one address twice, two addresses sharing a bucket in either order, 128 copies of one address, 128 distinct addresses in one bucket ascending and descending, and 128 spread across buckets in descending address order all park for their full deadline and answer ETIMEDOUT. A wake aimed at the second of two colliding entries returns index 1 on both. The dedup was correct; what it lacked was a statement of why. tests/test-futex-waitv-buckets.c is those cases minus the wake, which needs a second thread to say nothing the timeout cases do not. It builds its colliding set from the hash in proved/futexhash.h, so the sharing is constructed rather than hoped for; on a reference kernel, which buckets differently, the same sets are ordinary and still have to behave. --- mk/verify.mk | 9 ++ src/proved/futexwaitv.h | 83 +++++++++++++++ src/runtime/futex.c | 41 +++----- tests/test-futex-waitv-buckets.c | 171 +++++++++++++++++++++++++++++++ tests/test-matrix.sh | 2 + 5 files changed, 281 insertions(+), 25 deletions(-) create mode 100644 src/proved/futexwaitv.h create mode 100644 tests/test-futex-waitv-buckets.c diff --git a/mk/verify.mk b/mk/verify.mk index 1ba01dfb..28e019b3 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -421,6 +421,15 @@ VERIFY_FUTEXPI_SCAN := src/proved/futexpi.h VERIFY_FUTEXPI_CLAIM := for ANY bit pattern a guest can write to a PI lock word VERIFY_FUTEXPI_UNPROVED := the CAS loops around them stay test-covered +VERIFY_FUTEXWAITV_SRC := src/proved/futexwaitv.h +VERIFY_FUTEXWAITV_FCTS := futex_bucket_insert +VERIFY_FUTEXWAITV_MIN_GOALS ?= 36 +# typed: one flat array of unsigned, no aliasing question beside it. +VERIFY_FUTEXWAITV_MODEL := typed +VERIFY_FUTEXWAITV_SCAN := src/proved/futexwaitv.h +VERIFY_FUTEXWAITV_CLAIM := for ANY set of guest-chosen futex addresses +VERIFY_FUTEXWAITV_UNPROVED := the walk that calls it stays test-covered + VERIFY_PATHDEPTH_SRC := src/proved/pathdepth.h VERIFY_PATHDEPTH_FCTS := path_depth_push path_depth_pop VERIFY_PATHDEPTH_MIN_GOALS ?= 24 diff --git a/src/proved/futexwaitv.h b/src/proved/futexwaitv.h new file mode 100644 index 00000000..05a5d78a --- /dev/null +++ b/src/proved/futexwaitv.h @@ -0,0 +1,83 @@ +/* + * The bucket set a futex_waitv call locks, split out of waitv_collect_buckets + * in src/runtime/futex.c and proved here. + * + * sys_futex_waitv takes up to 128 guest-chosen addresses, hashes each to a + * bucket, and locks the distinct buckets in ascending index order. Two entries + * hashing alike is ordinary: there are 1024 buckets and the guest picks the + * addresses. What holds the call together is that this set comes out sorted and + * without repeats. A repeat locks one non-recursive mutex twice, and an + * unsorted set takes the bucket locks out of order against every other futex + * path. + * + * The insertion is proved rather than the walk around it: the walk's own bound + * is nr_futexes, which sys_futex_waitv checks before it gets here. + */ +#pragma once + +#include + +/*@ + predicate sorted_strict(unsigned *a, integer n) = + \forall integer i, j; 0 <= i < j < n ==> a[i] < a[j]; + + predicate holds(unsigned *a, integer n, unsigned v) = + \exists integer k; 0 <= k < n && a[k] == v; + */ + +/* Insert idx into a sorted, repeat-free prefix, and answer the new length. + * + * cap is the array's length rather than the caller's bound, so the shift below + * is inside the object for any n the precondition allows. + */ +/*@ + requires room: n < cap; + requires valid: \valid(ids + (0 .. cap - 1)); + requires sorted: sorted_strict(ids, n); + assigns ids[0 .. cap - 1]; + ensures grows_by_at_most_one: \result == n || \result == n + 1; + ensures still_sorted: sorted_strict(ids, \result); + ensures present: holds(ids, \result, idx); + ensures fresh_is_longer: + \result == n + 1 <==> !\at(holds(ids, n, idx), Pre); + */ +static inline unsigned futex_bucket_insert(unsigned *ids, + unsigned n, + unsigned cap, + unsigned idx) +{ + unsigned pos = 0; + + /*@ + loop invariant bound: 0 <= pos <= n; + loop invariant below: \forall integer i; 0 <= i < pos ==> ids[i] < idx; + loop assigns pos; + loop variant n - pos; + */ + while (pos < n && ids[pos] < idx) + pos++; + + if (pos < n && ids[pos] == idx) + return n; + + /* Nothing at or after pos equals idx either: the scan stopped at the first + * entry not below idx, and the prefix is strictly increasing. + */ + /*@ assert past: pos < n ==> ids[pos] > idx; */ + /*@ assert absent: !holds(ids, n, idx); */ + + /*@ + loop invariant bound: pos <= j <= n; + loop invariant shifted: + \forall integer k; j < k <= n ==> ids[k] == \at(ids[k - 1], LoopEntry); + loop invariant kept: + \forall integer k; 0 <= k < j ==> ids[k] == \at(ids[k], LoopEntry); + loop assigns j, ids[pos + 1 .. n]; + loop variant j - pos; + */ + for (unsigned j = n; j > pos; j--) + ids[j] = ids[j - 1]; + + ids[pos] = idx; + return n + 1; +} diff --git a/src/runtime/futex.c b/src/runtime/futex.c index 12c0499f..d5dc8f84 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -44,6 +44,7 @@ #include "proved/futexop.h" #include "proved/futexpi.h" #include "proved/futexreq.h" +#include "proved/futexwaitv.h" #include "proved/futexwakeop.h" #include "proved/timespec.h" @@ -2269,30 +2270,22 @@ typedef struct { #define LINUX_CLOCK_REALTIME 0 #define LINUX_CLOCK_MONOTONIC 1 +/* The distinct buckets the wait set covers, ascending. The locks below are + * taken in this order and released in reverse, so both properties of the answer + * are load-bearing: proved/futexwaitv.h carries them. + * + * nr_futexes is bounded by FUTEX_WAITV_MAX before the call, which is what keeps + * nbuckets below the array length at every insert. + */ static int waitv_collect_buckets(const linux_futex_waitv_t *elts, uint32_t nr_futexes, - unsigned bucket_ids[FUTEX_WAITV_MAX], - futex_bucket_t *bucket_ptrs[FUTEX_WAITV_MAX]) + unsigned bucket_ids[FUTEX_WAITV_MAX]) { unsigned nbuckets = 0; - for (uint32_t i = 0; i < nr_futexes; i++) { - unsigned idx = futex_hash(elts[i].uaddr); - unsigned pos = 0; - - while (pos < nbuckets && bucket_ids[pos] < idx) - pos++; - if (pos < nbuckets && bucket_ids[pos] == idx) - continue; - - for (unsigned j = nbuckets; j > pos; j--) { - bucket_ids[j] = bucket_ids[j - 1]; - bucket_ptrs[j] = bucket_ptrs[j - 1]; - } - bucket_ids[pos] = idx; - bucket_ptrs[pos] = &buckets[idx]; - nbuckets++; - } + for (uint32_t i = 0; i < nr_futexes; i++) + nbuckets = futex_bucket_insert(bucket_ids, nbuckets, FUTEX_WAITV_MAX, + futex_hash(elts[i].uaddr)); return (int) nbuckets; } @@ -2389,9 +2382,7 @@ int64_t sys_futex_waitv(guest_t *g, */ futex_waiter_t waiters[FUTEX_WAITV_MAX]; unsigned bucket_ids[FUTEX_WAITV_MAX]; - futex_bucket_t *bucket_ptrs[FUTEX_WAITV_MAX]; - int nbuckets = - waitv_collect_buckets(elts, nr_futexes, bucket_ids, bucket_ptrs); + int nbuckets = waitv_collect_buckets(elts, nr_futexes, bucket_ids); int enqueued = 0; int64_t result_err = 0; @@ -2414,7 +2405,7 @@ int64_t sys_futex_waitv(guest_t *g, } for (int i = 0; i < nbuckets; i++) - pthread_mutex_lock(&bucket_ptrs[i]->lock); + pthread_mutex_lock(&buckets[bucket_ids[i]].lock); for (uint32_t i = 0; i < nr_futexes; i++) { uint64_t uaddr = elts[i].uaddr; @@ -2443,7 +2434,7 @@ int64_t sys_futex_waitv(guest_t *g, } for (int i = nbuckets - 1; i >= 0; i--) - pthread_mutex_unlock(&bucket_ptrs[i]->lock); + pthread_mutex_unlock(&buckets[bucket_ids[i]].lock); /* All enqueued. Block on shared.cond until any wake site signals it. The * bounded sleep (capped at 100 ms or the user deadline, whichever is @@ -2526,7 +2517,7 @@ int64_t sys_futex_waitv(guest_t *g, unlock_early: for (int i = nbuckets - 1; i >= 0; i--) - pthread_mutex_unlock(&bucket_ptrs[i]->lock); + pthread_mutex_unlock(&buckets[bucket_ids[i]].lock); for (int i = enqueued - 1; i >= 0; i--) { waitv_unlink(&waiters[i]); diff --git a/tests/test-futex-waitv-buckets.c b/tests/test-futex-waitv-buckets.c new file mode 100644 index 00000000..e237cd65 --- /dev/null +++ b/tests/test-futex-waitv-buckets.c @@ -0,0 +1,171 @@ +/* + * futex_waitv over entries that share a bucket + * + * Copyright 2026 elfuse contributors + * SPDX-License-Identifier: Apache-2.0 + * + * elfuse locks one bucket per distinct address hash, ascending, and unlocks in + * reverse. Two guest addresses hashing alike is ordinary: there are 1024 + * buckets and the guest picks the addresses. A repeat in that set locks one + * non-recursive mutex twice, which is a hang rather than an errno, so every + * case here is bounded by a deadline the call has to answer. + * + * The hash below mirrors proved/futexhash.h. It only names elfuse's buckets; a + * reference kernel buckets differently, so there the same cases are ordinary + * wait sets and still have to behave. + * + * Syscalls exercised: futex_waitv(449), futex(98), clone(220), exit(93), + * clock_gettime(113) + */ + +#include +#include +#include +#include + +#include "test-harness.h" +#include "raw-syscall.h" +#include "test-util.h" + +int passes = 0, fails = 0; + +#define __NR_futex_waitv 449 +#define FUTEX2_SIZE_U32 0x02 +#define WAITV_MAX 128 + +/* Mirrors futex_bucket_index in proved/futexhash.h with FUTEX_BUCKETS. */ +#define FUTEX_HASH_MULT 0x9E3779B97F4A7C15ULL +#define FUTEX_BUCKETS 1024u + +struct futex_waitv { + uint64_t val; + uint64_t uaddr; + uint32_t flags; + uint32_t __reserved; +}; + +struct k_timespec { + int64_t tv_sec; + int64_t tv_nsec; +}; + +#define PARK_MS 200 +#define EARLY_MS (PARK_MS / 2) + +#define ARENA_WORDS (1u << 20) +static uint32_t arena[ARENA_WORDS]; +static int32_t first_at[FUTEX_BUCKETS]; +static int32_t shared[WAITV_MAX]; +static int n_shared; + +static uint32_t bucket_of(uint64_t a) +{ + return (uint32_t) (((((a >> 2) * FUTEX_HASH_MULT) >> 32)) % FUTEX_BUCKETS); +} + +static long now_ms(void) +{ + struct k_timespec ts; + raw_syscall2(113, 1 /* CLOCK_MONOTONIC */, (long) &ts); + return (long) (ts.tv_sec * 1000 + ts.tv_nsec / 1000000); +} + +static void deadline_in(struct k_timespec *ts, long ms) +{ + raw_syscall2(113, 1, (long) ts); + ts->tv_nsec += ms * 1000L * 1000L; + while (ts->tv_nsec >= 1000000000L) { + ts->tv_nsec -= 1000000000L; + ts->tv_sec++; + } +} + +static void fill(struct futex_waitv *w, int n, uint32_t *const *addrs) +{ + memset(w, 0, sizeof(*w) * (size_t) n); + for (int i = 0; i < n; i++) { + w[i].uaddr = (uint64_t) (uintptr_t) addrs[i]; + w[i].flags = FUTEX2_SIZE_U32; + } +} + +/* Every case waits out its deadline: nothing here is woken. A repeat in the + * bucket set never gets that far. + */ +static void expect_timeout(const char *name, struct futex_waitv *w, int n) +{ + TEST(name); + struct k_timespec ts; + deadline_in(&ts, PARK_MS); + long t0 = now_ms(); + long rc = raw_syscall5(__NR_futex_waitv, (long) w, n, 0, (long) &ts, 1); + long elapsed = now_ms() - t0; + + if (rc != -ETIMEDOUT) + FAIL("a wait set nobody wakes must report ETIMEDOUT"); + else if (elapsed < EARLY_MS) + FAIL("the wait did not last"); + else + PASS(); +} + +int main(void) +{ + printf("=== futex_waitv bucket sharing ===\n\n"); + + for (uint32_t i = 0; i < FUTEX_BUCKETS; i++) + first_at[i] = -1; + + /* One bucket's worth of distinct words, enough to fill a whole wait set. */ + uint32_t target = bucket_of((uint64_t) (uintptr_t) &arena[0]); + for (uint32_t i = 0; i < ARENA_WORDS && n_shared < WAITV_MAX; i++) + if (bucket_of((uint64_t) (uintptr_t) &arena[i]) == target) + shared[n_shared++] = (int32_t) i; + + TEST("arena yields a full shared bucket"); + if (n_shared < WAITV_MAX) { + FAIL("not enough words share one bucket"); + goto done; + } + PASS(); + + struct futex_waitv w[WAITV_MAX]; + uint32_t *addrs[WAITV_MAX]; + + for (int i = 0; i < 2; i++) + addrs[i] = &arena[shared[0]]; + fill(w, 2, addrs); + expect_timeout("one address twice", w, 2); + + addrs[0] = &arena[shared[0]]; + addrs[1] = &arena[shared[1]]; + fill(w, 2, addrs); + expect_timeout("two addresses, one bucket", w, 2); + + addrs[0] = &arena[shared[1]]; + addrs[1] = &arena[shared[0]]; + fill(w, 2, addrs); + expect_timeout("the same two, descending", w, 2); + + for (int i = 0; i < WAITV_MAX; i++) + addrs[i] = &arena[shared[0]]; + fill(w, WAITV_MAX, addrs); + expect_timeout("one address 128 times", w, WAITV_MAX); + + /* Descending is the insertion's worst case: every entry goes to the front + * and shifts the whole set. + */ + for (int i = 0; i < WAITV_MAX; i++) + addrs[i] = &arena[shared[WAITV_MAX - 1 - i]]; + fill(w, WAITV_MAX, addrs); + expect_timeout("128 in one bucket, descending", w, WAITV_MAX); + + for (int i = 0; i < WAITV_MAX; i++) + addrs[i] = &arena[(uint32_t) (WAITV_MAX - 1 - i) * 977u]; + fill(w, WAITV_MAX, addrs); + expect_timeout("128 spread, descending address", w, WAITV_MAX); + +done: + SUMMARY("test-futex-waitv-buckets"); + return fails > 0 ? 1 : 0; +} diff --git a/tests/test-matrix.sh b/tests/test-matrix.sh index 1ae28a6b..b8e0fb97 100755 --- a/tests/test-matrix.sh +++ b/tests/test-matrix.sh @@ -896,6 +896,8 @@ run_unit_tests() "$bindir/test-futex-requeue-pi" test_rc "$runner" "test-futex-wake-op-enosys" 0 \ "$bindir/test-futex-wake-op-enosys" + test_rc "$runner" "test-futex-waitv-buckets" 0 \ + "$bindir/test-futex-waitv-buckets" test_rc "$runner" "test-robust-futex" 0 "$bindir/test-robust-futex" test_check "$runner" "test-shim-futex-fast" "OK" \ "$bindir/test-shim-futex-fast" From 60b46cf1c4b8cfecf5ab60c5ce2504d2c8afd689 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:06:33 +0800 Subject: [PATCH 11/11] Make the futexwaitv gate bite Three mutations, each an ordinary way to write the insertion wrong: append without scanning, so the set stops being sorted; drop the repeat check, so a shared bucket is locked twice; and stop the scan one entry short, so an equal entry is missed and inserted again. All three are caught. The second is the one the contract exists for: it is not a wrong value but a hang, and no assertion in a test can observe it from inside the call that hangs. --- scripts/check-mutants.py | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index a2eb0fe5..b48538d7 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -196,6 +196,31 @@ def _load(stem, name): " return (uint64_t) nr_wake + nr_requeue;\n", " return (uint64_t) nr_requeue;\n", ), + # ---- verify-futexwaitv ------------------------------------------------- + ( + "futexwaitv", + "src/proved/futexwaitv.h", + "futex_bucket_insert", + "append without scanning (the set stops being sorted)", + " unsigned pos = 0;\n", + " unsigned pos = n;\n", + ), + ( + "futexwaitv", + "src/proved/futexwaitv.h", + "futex_bucket_insert", + "drop the repeat check (one bucket is locked twice)", + " if (pos < n && ids[pos] == idx)\n return n;\n", + " if (0)\n return n;\n", + ), + ( + "futexwaitv", + "src/proved/futexwaitv.h", + "futex_bucket_insert", + "stop the scan one short (an equal entry is missed)", + " while (pos < n && ids[pos] < idx)\n", + " while (pos + 1 < n && ids[pos] < idx)\n", + ), # ---- verify-futexpi ---------------------------------------------------- ( "futexpi",