Type and verify the wtc ops against what they lower to

README.md

@@ -16,7 +16,7 @@ what exists is one vertical slice and it is not finished:
 
 | Piece | State |
 | --- | --- |
-| `wtc` dialect: `mutex` and `queue<T>` types, `lock`, `unlock`, `queue_push`, `queue_pop` | defined; no verifiers, no memory-effect or progress semantics yet |
+| `wtc` dialect: `mutex` and `queue<T>` 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 |

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<T>`, 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.

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
 

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"

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<string mnemonic, list<Trait> traits = []> :
     Op<WTC_Dialect, mnemonic, traits>;
 
-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<string mnemonic, list<Trait> traits = []> :
+    WTC_Op<mnemonic, !listconcat(traits, [
+        DeclareOpInterfaceMethods<SymbolUserOpInterface>,
+        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<FlatSymbolRefAttr>:$fallback_impl,
         OptionalAttr<TypeAttr>:$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<FlatSymbolRefAttr>:$fallback_impl,
         OptionalAttr<TypeAttr>:$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<I64Attr>:$queue_id,
         OptionalAttr<FlatSymbolRefAttr>:$fallback_impl,
         OptionalAttr<TypeAttr>:$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<T> 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<FlatSymbolRefAttr>:$fallback_impl,
         OptionalAttr<TypeAttr>:$source_queue_type);
     let results = (outs Optional<AnyType>:$value);
+    let hasVerifier = 1;
 }
 
 #endif // WTC_OPS_TD

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)

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"
+#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_<name>_<operation>.
+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<cir::AnnotationAttr>(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<cir::FuncOp>(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<cir::PointerType>(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<QueueType>(getQueue().getType()), "the pushed value");
+}
+
+LogicalResult QueuePopOp::verify() {
+    if (static_cast<bool>(getResultSlot()) == static_cast<bool>(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<QueueType>(getQueue().getType()), "the popped value");
+    return success();
+}

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<s, 32>
+cir.func @lock_not_a_mutex(%p: !cir.ptr<!s32i>) {
+  // expected-error @+1 {{operand #0 must be}}
+  "wtc.lock"(%p) : (!cir.ptr<!s32i>) -> ()
+  cir.return
+}
+
+// -----
+
+// The value pushed must be a reference to the queue's element type.
+
+!s32i = !cir.int<s, 32>
+!s64i = !cir.int<s, 64>
+cir.func @push_wrong_type(%qp: !cir.ptr<!s32i>, %v: !cir.ptr<!s64i>) {
+  %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+  // expected-error @+1 {{the pushed value points to '!cir.int<s, 64>', but the queue holds '!cir.int<s, 32>'}}
+  "wtc.queue_push"(%q, %v) : (!wtc.queue<!s32i>, !cir.ptr<!s64i>) -> ()
+  cir.return
+}
+
+// -----
+
+// A pop delivers its value one way: as its result or through result_slot.
+
+!s32i = !cir.int<s, 32>
+cir.func @pop_both_ways(%qp: !cir.ptr<!s32i>, %slot: !cir.ptr<!s32i>) {
+  %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+  // 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<!s32i>, !cir.ptr<!s32i>) -> !cir.ptr<!s32i>
+  cir.return
+}
+
+// -----
+
+!s32i = !cir.int<s, 32>
+cir.func @pop_neither_way(%qp: !cir.ptr<!s32i>) {
+  %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+  // expected-error @+1 {{must either return the popped value or write it through result_slot, not neither}}
+  "wtc.queue_pop"(%q) : (!wtc.queue<!s32i>) -> ()
+  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<s, 32>
+module {
+  cir.func @push_to_nowhere(%qp: !cir.ptr<!s32i>, %v: !cir.ptr<!s32i>) {
+    %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+    // expected-error @+1 {{fallback_impl @missing does not name a cir.func}}
+    "wtc.queue_push"(%q, %v) {fallback_impl = @missing} : (!wtc.queue<!s32i>, !cir.ptr<!s32i>) -> ()
+    cir.return
+  }
+}
+
+// -----
+
+!s32i = !cir.int<s, 32>
+module {
+  cir.func private @not_a_push(!cir.ptr<!s32i>, !cir.ptr<!s32i>) [#cir.annotation<"wtc_queue_try_pop">]
+
+  cir.func @push_to_a_pop(%qp: !cir.ptr<!s32i>, %v: !cir.ptr<!s32i>) {
+    %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+    // 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<!s32i>, !cir.ptr<!s32i>) -> ()
+    cir.return
+  }
+}
+
+// -----
+
+!s32i = !cir.int<s, 32>
+module {
+  cir.func private @try_pop(!cir.ptr<!s32i>) -> !cir.ptr<!s32i> [#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<!s32i>, %slot: !cir.ptr<!s32i>) {
+    %q = builtin.unrealized_conversion_cast %qp : !cir.ptr<!s32i> to !wtc.queue<!s32i>
+    // 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<!s32i>, !cir.ptr<!s32i>) -> ()
+    cir.return
+  }
+}