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<{{.*}}>) -> ()