From ad2187d2e23d3d5fa69cfb46b769cbd4d444c99b Mon Sep 17 00:00:00 2001 From: zwe Date: Sun, 18 Oct 2026 12:34:39 +0800 Subject: [PATCH] Type and verify the wtc ops against what they lower to lock and unlock accepted an operand of any type, and nothing checked an op against the call it stands for: a wrong fallback_impl surfaced only when the lowered call failed to verify or link, if it did at all. Now lock and unlock take a !wtc.mutex. Push checks that the value it passes refers to the queue's element type; pop does the same for a pointer result, and delivers its value exactly one way, as its result or through result_slot. Each op checks that fallback_impl names a cir.func implementing the same operation -- the shim's annotation, or a substitute's wtc_impl__ -- that takes the arguments lowering will pass. Each op declares that it reads and writes memory. That is the mechanical part. What the ops promise about ordering and progress is a design question, so decisions/0003 proposes an answer for discussion rather than implementing one. Verified: 17 of 17 pass, no warnings. The seven invalid cases are all accepted silently by the parent commit. The prototype's example, lifted for AArch64 and for x86-64, verifies under the new rules. Co-Authored-By: Claude Opus 5.5 --- README.md | 2 +- ...03-concurrency-semantics-of-the-wtc-ops.md | 70 ++++++++++++ docs/audit.md | 12 +- mlir/include/WTC/WTCOps.h | 2 + mlir/include/WTC/WTCOps.td | 26 ++++- mlir/lib/WTC/CMakeLists.txt | 4 + mlir/lib/WTC/WTCOps.cpp | 103 +++++++++++++++++- test/Dialect/invalid.mlir | 90 +++++++++++++++ test/Dialect/ops.mlir | 35 ++++++ 9 files changed, 334 insertions(+), 10 deletions(-) create mode 100644 decisions/0003-concurrency-semantics-of-the-wtc-ops.md create mode 100644 test/Dialect/invalid.mlir create mode 100644 test/Dialect/ops.mlir diff --git a/README.md b/README.md index ba95722..6b4f89d 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ what exists is one vertical slice and it is not finished: | Piece | State | | --- | --- | -| `wtc` dialect: `mutex` and `queue` types, `lock`, `unlock`, `queue_push`, `queue_pop` | defined; no verifiers, no memory-effect or progress semantics yet | +| `wtc` dialect: `mutex` and `queue` types, `lock`, `unlock`, `queue_push`, `queue_pop` | defined and verified, including each op's `fallback_impl`; ordering and progress semantics proposed in `decisions/0003`, not yet adopted | | Lifting CIR calls into the dialect | works on hand-written IR; the C++ path is not yet exercised end to end | | Queue ownership analysis: SPSC / MPSC / SPMC / MPMC | prints a verdict; sound for direct calls, UNKNOWN wherever a function's address escapes; thread lifetime and escaping queues not modelled | | Lowering back to CIR | faithful round trip; crashes on operations that carry no source-type attribute | diff --git a/decisions/0003-concurrency-semantics-of-the-wtc-ops.md b/decisions/0003-concurrency-semantics-of-the-wtc-ops.md new file mode 100644 index 0000000..5b96162 --- /dev/null +++ b/decisions/0003-concurrency-semantics-of-the-wtc-ops.md @@ -0,0 +1,70 @@ +# 3. What a wtc operation promises about concurrency + +Proposed 2026-10-18. **Not yet taken**: written for discussion before any of +it is implemented. + +## Context + +The four ops now have types, verifiers, and a checked `fallback_impl`, and +each declares that it reads and writes memory. That last part says nothing +about concurrency. It makes every op an opaque barrier, which is safe for +transforms around it, and it is the only thing the IR says. An op still means +"a call to this function, recognised". + +That matters at substitution, not before. `--select-queue-impl` replaces +`wtc::queue`, which takes a mutex on every operation, with a lock-free +structure that synchronises through acquire and release. Whether that is a +correct substitution depends on what the program was entitled to rely on, +and today nothing writes that down. The answer is currently "whatever the +mutex happened to give", which is more than the substitute gives. + +## The questions + +**Ordering.** Every implementation must give the per-item guarantee: a push +happens-before the pop that returns its item. The mutex-based queue also +totally orders all operations on one queue, and orders them against the +program's other uses of mutexes. A program that uses an empty pop as a +signal ("the producer has not started yet") relies on that total order. The +SPSC substitute does not give it. + +**Linearisability and FIFO.** Both implementations are linearisable when used +as SPSC, and both are FIFO. With several producers, the only order defined +is each producer's own. + +**Progress.** The shim queue blocks on a mutex; the substitute is lock-free +on the consumer side, and its producer allocates. A program cannot observe +progress except as deadlock or starvation, and a substitution can only make +those less likely, not more. + +**Effects.** Per-object memory effects would let a transform reorder ops on +two different queues. In a concurrent program that is not generally sound, +since an op on one queue can be what orders an op on the other. The single +default resource is right until a model says otherwise. + +## Options + +1. **Keep "opaque call".** Nothing is promised and nothing is checked. Every + substitution is then justified only by its author's reading of the + program. +2. **Promise the minimal contract, per op kind, in the dialect's + documentation.** That is: per-item happens-before from a push to its pop; + linearisability per queue; FIFO per producer; no ordering against other + objects; no progress guarantee. A substitute's header states it meets the + contract. A program relying on more — empty-pop signalling, ordering + across queues — is outside what the dialect promises, and is not a + candidate for substitution. +3. **Carry an ordering attribute on each op**, modelled on LLVM's atomic + orderings, so that a stronger guarantee can be asked for where a program + needs it, and verified against the implementation chosen. + +## Proposal + +Option 2 now, with room for option 3 later. It costs a precise paragraph per +op and a promise in each `runtime/` header, and it turns "is this +substitution correct" into a question with a written answer. + +What it does not settle, and what the discussion should: whether the +analysis has to detect programs that rely on more than the contract (for +example, a pop whose emptiness is branched on and then followed by an +access to other shared state), or whether those are accepted as the +programmer's responsibility, as they would be for any library swap. diff --git a/docs/audit.md b/docs/audit.md index 11a4a86..15335a2 100644 --- a/docs/audit.md +++ b/docs/audit.md @@ -53,8 +53,16 @@ point. An operation currently amounts to a tagged call: one attribute holds the original function's name, another its original type. Nothing is expressed that CIR did not already say. -Typing is inconsistent: the queue operations constrain their operand to the -queue type, while `lock` and `unlock` accept anything. +Typing was inconsistent: the queue operations constrained their operand to the +queue type, while `lock` and `unlock` accepted anything. + +Fixed in October 2026, the mechanical part: `lock` and `unlock` take a +`!wtc.mutex`; push and pop check their values against the queue's element +type; `fallback_impl` must name a `cir.func` that implements the same +operation and takes the arguments lowering will pass; each op declares that +it reads and writes memory (`test/Dialect/invalid.mlir`). The concurrency +semantics proper are still open, and +`decisions/0003-concurrency-semantics-of-the-wtc-ops.md` proposes them. ## Lowering crashes on hand-written IR — fixed diff --git a/mlir/include/WTC/WTCOps.h b/mlir/include/WTC/WTCOps.h index eb3de1c..ca5b566 100644 --- a/mlir/include/WTC/WTCOps.h +++ b/mlir/include/WTC/WTCOps.h @@ -3,6 +3,8 @@ #include "mlir/Bytecode/BytecodeOpInterface.h" #include "mlir/IR/OpDefinition.h" +#include "mlir/IR/SymbolTable.h" +#include "mlir/Interfaces/SideEffectInterfaces.h" #include "WTC/WTCDialect.h" #include "WTC/WTCTypes.h" diff --git a/mlir/include/WTC/WTCOps.td b/mlir/include/WTC/WTCOps.td index f9d6a9e..ca6acb4 100644 --- a/mlir/include/WTC/WTCOps.td +++ b/mlir/include/WTC/WTCOps.td @@ -2,36 +2,49 @@ #define WTC_OPS_TD include "mlir/IR/OpBase.td" +include "mlir/IR/SymbolInterfaces.td" +include "mlir/Interfaces/SideEffectInterfaces.td" include "WTC/WTCDialect.td" include "WTC/WTCTypes.td" class WTC_Op traits = []> : Op; -def LockOp : WTC_Op<"lock"> { +// Every wtc op stands for a call it can be lowered back to, named by +// fallback_impl and checked against it. Each one reads and writes the +// object it is given; nothing finer is claimed yet. What the ops guarantee +// about ordering and progress is an open design question +// (decisions/0003). +class WTC_ObjectOp traits = []> : + WTC_Op, + MemoryEffects<[MemRead, MemWrite]>])>; + +def LockOp : WTC_ObjectOp<"lock"> { let summary = "A mutex lock operation"; - let arguments = (ins AnyType:$mutex, + let arguments = (ins WTC_MutexType:$mutex, OptionalAttr:$fallback_impl, OptionalAttr:$source_mutex_type); } -def UnlockOp : WTC_Op<"unlock"> { +def UnlockOp : WTC_ObjectOp<"unlock"> { let summary = "A mutex unlock operation"; - let arguments = (ins AnyType:$mutex, + let arguments = (ins WTC_MutexType:$mutex, OptionalAttr:$fallback_impl, OptionalAttr:$source_mutex_type); } -def QueuePushOp : WTC_Op<"queue_push", []> { +def QueuePushOp : WTC_ObjectOp<"queue_push"> { let summary = "A queue push operation"; let arguments = (ins WTC_QueueType:$queue, AnyType:$value, OptionalAttr:$queue_id, OptionalAttr:$fallback_impl, OptionalAttr:$source_queue_type); let results = (outs); + let hasVerifier = 1; } -def QueuePopOp : WTC_Op<"queue_pop", []> { +def QueuePopOp : WTC_ObjectOp<"queue_pop"> { let summary = "A non-blocking queue pop operation, mirroring shared_ptr semantics: a null result means empty"; let description = [{ The popped value is either the op's result or, where the target ABI @@ -45,6 +58,7 @@ def QueuePopOp : WTC_Op<"queue_pop", []> { OptionalAttr:$fallback_impl, OptionalAttr:$source_queue_type); let results = (outs Optional:$value); + let hasVerifier = 1; } #endif // WTC_OPS_TD \ No newline at end of file diff --git a/mlir/lib/WTC/CMakeLists.txt b/mlir/lib/WTC/CMakeLists.txt index 59acef3..ec1c0ca 100644 --- a/mlir/lib/WTC/CMakeLists.txt +++ b/mlir/lib/WTC/CMakeLists.txt @@ -9,7 +9,11 @@ add_mlir_dialect_library(MLIRWTC MLIRWTCTypesIncGen LINK_LIBS PUBLIC + # The verifiers check push and pop against CIR types and fallback_impl + # against the cir.func it names. + MLIRCIR MLIRIR + MLIRSideEffectInterfaces ) add_subdirectory(Transforms) \ No newline at end of file diff --git a/mlir/lib/WTC/WTCOps.cpp b/mlir/lib/WTC/WTCOps.cpp index 60b5e65..23a9b7c 100644 --- a/mlir/lib/WTC/WTCOps.cpp +++ b/mlir/lib/WTC/WTCOps.cpp @@ -1,7 +1,108 @@ #include "WTC/WTCOps.h" +#include "clang/CIR/Dialect/IR/CIRAttrs.h" +#include "clang/CIR/Dialect/IR/CIRDialect.h" +#include "clang/CIR/Dialect/IR/CIRTypes.h" + #include "mlir/IR/Builders.h" #include "mlir/IR/OpImplementation.h" +#include "mlir/IR/SymbolTable.h" #define GET_OP_CLASSES -#include "WTC/WTCOps.cpp.inc" \ No newline at end of file +#include "WTC/WTCOps.cpp.inc" + +using namespace mlir; +using namespace mlir::wtc; + +namespace { + +// A function implements an operation if it carries the shim's annotation +// for it, or a substitute implementation's: wtc_impl__. +bool implementsOperation(cir::FuncOp func, StringRef shimAnnotation, StringRef operation) { + auto annotations = func.getAnnotationsAttr(); + if (!annotations) + return false; + for (Attribute attr : annotations) { + auto annotation = mlir::dyn_cast(attr); + if (!annotation) + continue; + StringRef name = annotation.getName().getValue(); + if (name == shimAnnotation) + return true; + if (name.starts_with("wtc_impl_") && name.ends_with(("_" + operation).str())) + return true; + } + return false; +} + +// fallback_impl is optional, but when present it has to be something the op +// can actually be lowered to: a cir.func implementing the same operation and +// taking the arguments the lowering will pass. +LogicalResult verifyFallbackImpl(Operation *op, FlatSymbolRefAttr impl, + StringRef shimAnnotation, StringRef operation, + unsigned expectedArgs, + SymbolTableCollection &symbolTable) { + if (!impl) + return success(); + + auto func = symbolTable.lookupNearestSymbolFrom(op, impl); + if (!func) + return op->emitOpError("fallback_impl ") << impl << " does not name a cir.func"; + + if (!implementsOperation(func, shimAnnotation, operation)) + return op->emitOpError("fallback_impl ") << impl << " is not annotated " + << shimAnnotation << " or wtc_impl_*_" << operation; + + if (func.getNumArguments() != expectedArgs) + return op->emitOpError("fallback_impl ") << impl << " takes " + << func.getNumArguments() << " arguments, but lowering passes " << expectedArgs; + + return success(); +} + +// The value pushed is passed by reference, and a pop that returns a pointer +// returns one to the element; either way the pointee has to be the queue's +// element type. Anything else -- the shared_ptr try_pop returns -- is +// accepted, since nothing here knows its layout. +LogicalResult verifyPointsToElement(Operation *op, Type type, QueueType queueType, + StringRef what) { + auto ptrType = mlir::dyn_cast(type); + if (!ptrType || ptrType.getPointee() == queueType.getElementType()) + return success(); + return op->emitOpError() << what << " points to " << ptrType.getPointee() + << ", but the queue holds " << queueType.getElementType(); +} + +} + +LogicalResult LockOp::verifySymbolUses(SymbolTableCollection &symbolTable) { + return verifyFallbackImpl(*this, getFallbackImplAttr(), "wtc_mutex_lock", "lock", 1, symbolTable); +} + +LogicalResult UnlockOp::verifySymbolUses(SymbolTableCollection &symbolTable) { + return verifyFallbackImpl(*this, getFallbackImplAttr(), "wtc_mutex_unlock", "unlock", 1, symbolTable); +} + +LogicalResult QueuePushOp::verifySymbolUses(SymbolTableCollection &symbolTable) { + return verifyFallbackImpl(*this, getFallbackImplAttr(), "wtc_queue_push", "push", 2, symbolTable); +} + +LogicalResult QueuePopOp::verifySymbolUses(SymbolTableCollection &symbolTable) { + unsigned expectedArgs = getResultSlot() ? 2 : 1; + return verifyFallbackImpl(*this, getFallbackImplAttr(), "wtc_queue_try_pop", "try_pop", expectedArgs, symbolTable); +} + +LogicalResult QueuePushOp::verify() { + return verifyPointsToElement(*this, getValue().getType(), + mlir::cast(getQueue().getType()), "the pushed value"); +} + +LogicalResult QueuePopOp::verify() { + if (static_cast(getResultSlot()) == static_cast(getValue())) + return emitOpError("must either return the popped value or write it through " + "result_slot, not ") << (getValue() ? "both" : "neither"); + if (Value value = getValue()) + return verifyPointsToElement(*this, value.getType(), + mlir::cast(getQueue().getType()), "the popped value"); + return success(); +} diff --git a/test/Dialect/invalid.mlir b/test/Dialect/invalid.mlir new file mode 100644 index 0000000..e6341ac --- /dev/null +++ b/test/Dialect/invalid.mlir @@ -0,0 +1,90 @@ +// RUN: wtc-opt %s -split-input-file -verify-diagnostics + +// lock and unlock used to accept an operand of any type; the queue ops +// already constrained theirs. + +!s32i = !cir.int +cir.func @lock_not_a_mutex(%p: !cir.ptr) { + // expected-error @+1 {{operand #0 must be}} + "wtc.lock"(%p) : (!cir.ptr) -> () + cir.return +} + +// ----- + +// The value pushed must be a reference to the queue's element type. + +!s32i = !cir.int +!s64i = !cir.int +cir.func @push_wrong_type(%qp: !cir.ptr, %v: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{the pushed value points to '!cir.int', but the queue holds '!cir.int'}} + "wtc.queue_push"(%q, %v) : (!wtc.queue, !cir.ptr) -> () + cir.return +} + +// ----- + +// A pop delivers its value one way: as its result or through result_slot. + +!s32i = !cir.int +cir.func @pop_both_ways(%qp: !cir.ptr, %slot: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{must either return the popped value or write it through result_slot, not both}} + %r = "wtc.queue_pop"(%q, %slot) : (!wtc.queue, !cir.ptr) -> !cir.ptr + cir.return +} + +// ----- + +!s32i = !cir.int +cir.func @pop_neither_way(%qp: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{must either return the popped value or write it through result_slot, not neither}} + "wtc.queue_pop"(%q) : (!wtc.queue) -> () + cir.return +} + +// ----- + +// fallback_impl has to name something the op can be lowered to. Before, a +// wrong one surfaced only when the lowered call failed to verify or link. + +!s32i = !cir.int +module { + cir.func @push_to_nowhere(%qp: !cir.ptr, %v: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{fallback_impl @missing does not name a cir.func}} + "wtc.queue_push"(%q, %v) {fallback_impl = @missing} : (!wtc.queue, !cir.ptr) -> () + cir.return + } +} + +// ----- + +!s32i = !cir.int +module { + cir.func private @not_a_push(!cir.ptr, !cir.ptr) [#cir.annotation<"wtc_queue_try_pop">] + + cir.func @push_to_a_pop(%qp: !cir.ptr, %v: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{fallback_impl @not_a_push is not annotated wtc_queue_push or wtc_impl_*_push}} + "wtc.queue_push"(%q, %v) {fallback_impl = @not_a_push} : (!wtc.queue, !cir.ptr) -> () + cir.return + } +} + +// ----- + +!s32i = !cir.int +module { + cir.func private @try_pop(!cir.ptr) -> !cir.ptr [#cir.annotation<"wtc_queue_try_pop">] + + // With a result slot, lowering passes two arguments; this callee takes one. + cir.func @pop_slot_mismatch(%qp: !cir.ptr, %slot: !cir.ptr) { + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + // expected-error @+1 {{fallback_impl @try_pop takes 1 arguments, but lowering passes 2}} + "wtc.queue_pop"(%q, %slot) {fallback_impl = @try_pop} : (!wtc.queue, !cir.ptr) -> () + cir.return + } +} diff --git a/test/Dialect/ops.mlir b/test/Dialect/ops.mlir new file mode 100644 index 0000000..1b1799b --- /dev/null +++ b/test/Dialect/ops.mlir @@ -0,0 +1,35 @@ +// RUN: wtc-opt %s | wtc-opt | FileCheck %s + +// Every op in a valid form, including a fallback_impl that names a +// substitute implementation rather than the shim, survives printing and +// parsing again. + +!s32i = !cir.int +!mutex = !cir.struct<"wtc::mutex" {data !s32i}> +!shared_ptr_i32 = !cir.struct<"std::shared_ptr" {data !cir.ptr, data !cir.ptr}> + +module { + cir.func private @lock(!cir.ptr) [#cir.annotation<"wtc_mutex_lock">] + cir.func private @unlock(!cir.ptr) [#cir.annotation<"wtc_mutex_unlock">] + cir.func private @spsc_push(!cir.ptr, !cir.ptr) [#cir.annotation<"wtc_impl_spsc_push">] + cir.func private @try_pop(!cir.ptr) -> !shared_ptr_i32 [#cir.annotation<"wtc_queue_try_pop">] + cir.func private @try_pop_sret(!cir.ptr {llvm.sret = !shared_ptr_i32}, !cir.ptr) [#cir.annotation<"wtc_queue_try_pop">] + + cir.func @all(%mp: !cir.ptr, %qp: !cir.ptr, %v: !cir.ptr, %slot: !cir.ptr) { + %m = builtin.unrealized_conversion_cast %mp : !cir.ptr to !wtc.mutex + %q = builtin.unrealized_conversion_cast %qp : !cir.ptr to !wtc.queue + "wtc.lock"(%m) {fallback_impl = @lock} : (!wtc.mutex) -> () + "wtc.unlock"(%m) {fallback_impl = @unlock} : (!wtc.mutex) -> () + "wtc.queue_push"(%q, %v) {fallback_impl = @spsc_push} : (!wtc.queue, !cir.ptr) -> () + %r = "wtc.queue_pop"(%q) {fallback_impl = @try_pop} : (!wtc.queue) -> !shared_ptr_i32 + "wtc.queue_pop"(%q, %slot) {fallback_impl = @try_pop_sret} : (!wtc.queue, !cir.ptr) -> () + cir.return + } +} + +// CHECK-LABEL: cir.func @all +// CHECK: "wtc.lock" +// CHECK: "wtc.unlock" +// CHECK: "wtc.queue_push"({{.*}}) <{fallback_impl = @spsc_push}> +// CHECK: "wtc.queue_pop"({{.*}}) <{fallback_impl = @try_pop}> : (!wtc.queue) -> !rec +// CHECK: "wtc.queue_pop"({{.*}}, {{.*}}) <{fallback_impl = @try_pop_sret}> : (!wtc.queue, !cir.ptr<{{.*}}>) -> ()