[RFC] Add a Builtin Token Type to MLIR

MLIR
1

TL;DR

Add a new builtin SSA value type (!token) to MLIR. A token is a value-typed handle that exists purely to encode a static def-use relationship between operations / regions. Think of a token as a pointer to another operation / region, reusing MLIR’s existing def-use machinery. Tokens cannot flow through “regular” value-forwarding constructs (cf.br, func.call, scf.for iter-args, region results, etc.).

This RFC is about the token type. This RFC is a continuation of the EuroLLVM 2026 round table on early exit and the follow-up discussion on Discourse.

This RFC was authored / discussed by: @gysit, @jpienaar, @matthias-springer, @mehdi_amini, @rengolin, @xheno.

Assisted-by: claude-opus-4.7-thinking-high

Open Questions

We are seeking feedback from the broader audience. Especially but not limited to:

  1. Minor question: A new builtin type or a new builtin type interface?
  2. Major question: Should the presence of tokens automatically (by design) affect CSE / DCE? If so, how and by what mechanism? See “5. Token is a unique opaque value in SSA scope” and “Interaction with Existing Infrastructure”.

Motivation

MLIR has several places where an operation needs to reference another specific operation or region in the IR — not a runtime value. Examples:

  1. Early exit from structured regions. A break/continue-like terminator must identify which enclosing operation it transfers control to (example). Proposed designs use integer “depth” counters, symbol labels, or new Operation references. All of these require renumbering, uniquing, or extending the core data structure and its bytecode/textual format.
  2. LLVM dialect fidelity. LLVM IR has a token type. It is used by Windows EH funclets (catchpad/cleanuppad/catchswitch), GC statepoints, preallocated arguments, and convergence intrinsics (llvm.experimental.convergence.*). The LLVM dialect cannot faithfully represent these without a value that is forbidden from appearing in phi, select, function arguments, etc.
  3. Exception handling and cleanups in front-end dialects. CIR already uses a token-like value in its cleanup/EH design to thread structural relationships between try, cleanup scopes, and unwind targets.
  4. High-level coroutine and convergence modeling. Anywhere a producer–consumer relationship must survive transformation but must not be substitutable, forwarded, or passed across function boundaries.
  5. Linking two operations that model a concept. E.g., linking operations for loop-carried variables and yield operands when modeling a loop via separate ops. (E.g., see TF Executor example at the end.)

In all of these cases the property we want is the same:

“This operand of op B must statically refer to a particular result/block-argument of op A. The link is structural; it carries no runtime data; transformations must not break it.”

A first-class builtin !token type lets us solve the problem once.

Non-goals

  • This RFC does not propose any specific scf.break/scf.continue design. That belongs in a follow-up RFC.
  • This RFC does not subsume !async.token. !async.token is a runtime, dataflow-carrying value (it represents a future). The new type is purely structural.
  • This RFC does not change Operation, the bytecode format, or the generic op syntax.

Intuition: A Token is a Static Reference to an Operation or Region

Every token use is — by construction — a reference to exactly one of:

  • an operation result (the op that produced the token), or
  • an entry block argument (which transitively identifies the block, its parent region, and the op that owns the region).

What makes the token type special is just that the SSA def–use edge is guaranteed to be static. With a normal value type, the def–use chain can be obscured by arith.select, cf.br block arguments, func.call boundaries, scf.for iter-args, etc., so you can’t generally walk back from a use and say “this came from that specific op”. With !token, you can.

This is also why tokens cannot be forwarded through calls, branches, selects, iter-args, and similar constructs. To be clear: any of those ops may legitimately produce a token as one of its results — but doing so just means the token refers to that producing op. There is no data flow. What is forbidden is taking a token in as an operand and re-emitting it (or one of several alternatives) as a result, so that downstream users can no longer tell which op the token refers to. For example, a cf.br that joins two predecessors, a call that crosses a function boundary, or an arith.select between two tokens would each make the answer to “which producer?” ambiguous or unknowable, and the type would lose the one property it exists to guarantee.

So !token is essentially a lightweight, SSA-native stand-in for Operation* / BlockArgument* references — without changing struct Operation, without a parallel use-list system, and without giving up dominance/region-scoping checks. Compared to other ways one might encode such a static reference:

  • vs. an Operation* operand on Operation: same expressive power for “which op am I referring to?”, but reuses the existing Value/OpOperand machinery instead of introducing a parallel use-list system for ops.
  • vs. symbol labels: same expressive power, but the lookup is just following an SSA edge instead of resolving a name through a side table, and uniquing falls out of SSA value identity.
  • vs. integer “depth” indices: an integer says “the N-th enclosing op of some kind”; a token says “that op”, so it’s stable when changing the nesting level without renumbering. Tokens also support relationships between sibling operations in a region (when the token is an op result) while numbering is only an alternative to tokens as block arguments (referring to a parent).

One nuance: a token can identify finer granularity than just the op. Because a token can be a n entry block argument, dialects can use it to refer to a specific region of a multi-region op (e.g. each region of scf.loop has its own entry-block token; all identify the same loop op but are distinguishable from each other). LLVM’s EH funclets rely on this distinction too — a catchpad token identifies a specific pad, not just the enclosing function.

Proposal

A New Builtin Type

Add a new builtin type, tentatively named !token (other candidates discussed below). It is a parameterless, opaque type with the following properties:

  • It is an ordinary SSA value type — it can appear as an operation result or block argument and has the usual Value/OpOperand machinery and use lists.
  • It carries no runtime representation. Lowerings are expected to consume tokens entirely; they have no LLVM-level analogue (other than LLVMTokenType, which uses the same name for a similar reason).
  • It has restricted structural semantics enforced by the framework (see below).

%t = some.op : !token

%x = some.consumer %t : !token -> i32

Note: Instead of a builtin type, the new token could also be a builtin type interface.

Structural Restrictions

A token value is, by construction:

  1. Not value-forwarding. A token cannot appear as a forwarded value anywhere — that is, anywhere the framework would treat it as data flowing from one program point to another rather than as a fixed reference to its producer. Concretely, a token cannot be:
    —
    1.1. a forwarded result or operand (getArgOperands) of a CallOpInterface op,
    —
    1.2. a result of, or an argument or result type of, a FunctionOpInterface op (note: a token block argument inside a function body is fine — it just identifies that block; what’s disallowed is forwarding tokens across the call/return boundary),
    —
    1.3. a successor operand or successor block argument of a BranchOpInterface op (e.g. cf.br, cf.cond_br),
    —
    1.4. a forwarded operand to/from any region of a RegionBranchOpInterface op — including iter-args, region results, and yielded values (e.g. scf.for iter-args, scf.if/scf.while results, scf.yield operands), or
    —
    1.5. the result of any op that selects or merges values it does not understand (e.g. arith.select).
    —
    These rules are enforced by op verifiers on the relevant interfaces (CallOpInterface, FunctionOpInterface, BranchOpInterface, RegionBranchOpInterface) plus the default ODS predicate change described in ODS integration below, so that an op which has not explicitly opted in cannot accept a token as an arbitrary operand.

  2. Transparent to IsolatedFromAbove. getUsedValuesDefinedAbove / visitUsedValuesDefinedAbove / region isolation verifiers filter tokens out by default. A token used inside an isolated region but defined above is not a capture, because no runtime data is being captured.

  3. Statically resolvable. For any token use, walking the def–use chain reaches a producing op without crossing a “forwarding” boundary. Verifiers and lowerings may rely on this.

  4. Cannot constant-fold. No constant of !token exists.

  5. Token is a unique opaque value in SSA scope: each token has its unique identity within the current region (and nested ones). This property has consequences for transformations such as CSE. This part is still a bit unclear and there are multiple possible options (5.1 - 5.3) to implement this property:
    —
    5.1. Operation Equivalence: Two operations in the same region aren’t equivalent if they involve different tokens. When comparing operations in different regions, a structural equivalence is performed.
    Downside: This makes operation equivalence contextual. Comparing two operations in isolation may be different from comparing two regions.
    —
    5.2. Operation Side Effect: A token-producing operation declares an AllocateToken side effect, which prevents the operation from CSE’ing. Special handling can be added to the CSE pass to enable CSE’ing of regions with nested tokens.
    Downside: Side effects are describing things that happen outside of SSA dataflow. Introducing side-effects into the token modeling makes it no longer a pure SSA representation and defeats most of the usefulness of a new construct. Side-effects are costly and pessimize / deactivate most optimizations.
    —
    5.3. Defined by Op Semantics: Drop the “5. Token is unique” property entirely and leave it up to the token-producing op. E.g., if CSE’ing of token-producing ops is desirable in your dialect, mark the op as pure. If not, leave the side effects unspecified (or add a AllocateToken effect), or utilize an IR design pattern that cannot be CSE’d (e.g., tokens are always block arguments).

These properties mirror what LLVM already documents for its own token type (“a value … all uses of [which] must not attempt to introspect or obscure it … not appropriate to have a phi or select of type token”). We are essentially lifting that contract into MLIR, where it is needed for more than just LLVM EH.

Verification

There are two ways a token could end up in a forwarding position, and each is already covered by an existing verification layer:

  • Ops that take operands of specific types (the vast majority). Their operand types are declared in ODS using AnyType, AnyTypeOf, etc. We update those predicates to exclude !token by default, so any such op simply will not type-check with a token operand. No new verifier is needed.
  • Ops that legitimately accept arbitrary types in forwarded positions. These all go through one of a small handful of interfaces: CallOpInterface, FunctionOpInterface, BranchOpInterface, and RegionBranchOpInterface. Their existing interface verifiers gain a check that none of the forwarded positions (call/return operands and results, function signature, successor operands, region forwarded operands, region results, yielded values) has token type.

Together, these two layers ensure that no token can reach a forwarding position regardless of which op it flows through. There is no need for a global walk over the IR.

Dialects that produce or consume tokens (e.g. scf, llvm, cir) additionally keep their own local contract checks — for example, “every user of this block-argument token must be a region terminator of this op”. Those are op-specific and orthogonal to the framework-level non-forwarding guarantee above.

ODS Integration

Most of the framework’s existing type predicates (AnyType, AnyTypeOf<[...]>, etc.) must continue to exclude tokens by default, so that no existing op accidentally accepts them.

Concretely:

  • Update AnyType to (conceptually) Type<CPred<"!::llvm::isa<::mlir::TokenType>($_self)">, "any non-token type"> (or a similar check).
  • Add AnyTypeOrToken as an explicit opt-in.
  • Add Token : Type<CPred<"::llvm::isa<::mlir::TokenType>($_self)">, "token", "::mlir::TokenType"> for ops that take a token specifically.
  • Example in TableGen: let arguments = (ins Token:$scope, AnyType:$value);.

No changes are needed to the ODS backends; this is just predicate plumbing.

Bytecode, Textual Format, and Printing

  • Textual: the type prints as !token (or whatever name we settle on). No new syntax.
  • Generic op syntax: unchanged. Tokens flow through as ordinary SSA values.
  • Bytecode: a new builtin type entry. No changes to op encoding.
  • Custom assembly: dialects can choose to pretty-print tokens (mirroring how scf.for pretty-prints the induction variable). This is a per-dialect choice, not a framework requirement.

Interaction with Existing Infrastructure

Area Behavior
Operation Equivalence We discussed if tokens should have a unique identity within the same SSA scope and how this affects operation equivalence. Should two otherwise equivalent token-producing ops compare as “not equivalent” if they are within the same SSA scope? This felt wrong because it makes equivalence checking contextual. (E.g., checking ops in isolation vs. within a region may give different results.)
CSE It is still unclear how (or if) the presence of token OpResults would affect CSE.
DCE It is still unclear if the presence of token OpResults should prevent DCE.
Canonicalization There is nothing new here.
Outlining Outlining IR into a function is potentially dangerous: you cannot pass a token across function boundaries.
Data Flow Framework Tokens carry no data flow.
IRMapping / clone Standard remapping; the type is a normal Type.
LICM / Hoisting Standard rules apply. SSA edge prevents hoisting too far out.
Loop Unrolling Note: Duplicating the loop body may introduce additional users of a token.

Lowering

Tokens usually get eliminated by lowerings, but this is very target specific. A common case of lowering is using the token relation during lowering, and dropping it when emitting the target construct that does need the token (e.g. scf.loop + its scf.break are lowered to cf.brs into a common exit block; the token disappears).

It is however possible to imagine targeting a bytecode or runtime environment directly consuming loops with early exits. In this case the tokens would be directly consumed by the target environment.

Naming

Options:

  • !token — short, mirrors LLVM. Risk: people read “token” as “async token” or “lexer token”.
  • !tok — shorter, avoids conflict with existing mentions of “token”. Risk: slightly obfuscated?
  • !structural_token — descriptive, longer.
  • !scope_token / !control_token — biased toward the early-exit use case.

Code Examples

Early Exit from Structure Loop (Original Use Case)

%r = scf.loop -> i32 {
^bb0(%t: !token):
  scf.if %cond {
    scf.break %t, %value : !token, i32
  }
  scf.continue %t : !token
}

The token is an entry-block argument of the loop region. scf.break and scf.continue take it as an operand. The scf.loop verifier checks that all users of %t are region terminators belonging to one of its regions; the builtin verifier guarantees no one smuggled %t out through a cf.br, func.call, etc.

LLVM dialect EH funclets (Faithful Modeling)

^catch:
  %cp = llvm.catchpad within %cs [%type_info] : !llvm.token
  // TODO rejected: !llvm.token cannot be a call argument
  llvm.call @handler(%cp) : (!llvm.token) -> ()
  llvm.catchret from %cp to ^continue : !llvm.token

Today, LLVMTokenType exists but the framework cannot prevent it from leaking through func.call or block arguments. With this proposal, those misuses are rejected by construction.

Rejected IR Examples

// Rejected: token captured by a non-token-aware op.
%t = scf.loop -> i32 { ^bb0(%tok: !token): ... }
%bad = arith.select %c, %tok, %tok2 : !token

// Rejected: token passed across a call boundary.
func.func @f(%t: !token) { ... } // function type contains !token
%r = func.call @f(%tok) : (!token) -> () // verifier error
// (A token block argument *inside* a function body is fine — what's
// rejected is having a token as part of the function's signature, so
// that callers cannot forward tokens across the call.)

// Rejected: token forwarded as an scf.for iter-arg.
%out = scf.for %i = %lb to %ub step %s iter_args(%x = %tok) -> !token { ... }

Modeling Loops with Multiple Ops in Graph Region

This example is taken from TensorFlow (semantics). The abstraction has been deprecated / removed.

tf_executor.graph {
  // A loop with 2 loop-carried variables.
  // Note: You cannot CSE/DCE these. Doing so would reduce the number of
  // loop-carried variables.
  %a_next, %a_token = NextIteration.Source
  %b_next, %b_token = NextIteration.Source

  // …

  // Token identifies which loop-carried variable gets which yielded value.
  NextIteration.Sink [%a_token], %yield_value_a
  NextIteration.Sink [%b_token], %yield_value_b
}

Implementation Plan

  1. Add mlir::TokenType in BuiltinTypes.{td,h,cpp}.
  2. Update AnyType predicate; add Token and AnyTypeOrToken predicates in CommonTypeConstraints.td.
  3. Possibly extend the verifiers of CallOpInterface, FunctionOpInterface, BranchOpInterface, and RegionBranchOpInterface to reject tokens in their forwarded positions; however this would be redundant with the AnyType verifier already checking this at the op level everywhere. This would only be useful for operations not defined in ODS, thus may not be a good tradeoff.
  4. Teach getUsedValuesDefinedAbove to filter tokens.
  5. Add bytecode entry.
  6. Documentation: BuiltinTypes.md and a short Tokens.md design note.
  7. Migrate LLVMTokenType to be (or wrap) the new builtin type, so EH/GC/convergence ops get the structural checks for free.
  8. (Follow-up RFC) Use !token to express early exit in scf.

Steps 1–6 are self-contained and can land before any user dialect adopts the type. Step 7 is the first real consumer.

2

I’d like to get the discussion started with my personal opinion on CSE / DCE / token uniqueness (Structural Restriction number 5).

My current thinking is that these are orthogonal to tokens and should be controlled by op semantics.

  • The presence of tokens would not affect CSE. Standard rules apply.
  • The presence of tokens would not affect DCE. Standard rules apply.
  • If a token-producing op wants to prevent CSE / DCE, it can work with the existing mechanisms.
    • E.g.: Adding an identifier attribute to the token-producing op would make them non-equivalent for OperationEquivalence and prevent CSE.
    • E.g.: Adding a side effect to the token-producing op (or leaving side effects unspecified) would prevent CSE / DCE.
    • E.g.: Defining a token as a region block argument would prevent CSE / DCE of the token.
  • If a token-producing op wants to CSE / DCE, mark it as Pure.

Basically, I am advocating for Option “5.3. Defined by Op Semantics”.

3

Could you summarize why the restriction? I understand that it is so tokens are completely static, but what is the advantage of adding a new edge case to SSA values to achieve this goal? I can’t imagine why make it illegal instead of for example bailing when it happens/rejecting it in verifiers for operations that care about that (for some reason? I can’t imagine a verifier that would care exclusively about that).

4

This is modeled after the LLVM token type, which cannot be passed to phi nodes. Disallowing tokens in unsupported places by construction will give better type safety.

rejecting it in verifiers for operations that care about that

This would be another option: The verifier of RegionBranchOpInterface and BranchOpInterface could verify that none of the forwarded operands are tokens. Most operations expect specific types and not many operations have AnyType operands/results. So in practice, adding verification to only control flow operations (i.e., not modifying the AnyType predicate) would give a similar level of safety.

5

Thank you for the RFC! Couple of comments:

Let’s make it an interface, that way we can recognize what the token is without doing a more complicated traversal. That is, control-flow tokens will get their dedicated interface to explicitly separate them.

I have some token types downstream that fit this exact token model (ie. we forbid them to flow), and I would like to easily pick what they are supposed to be based on the type.

IMO this is fragile and a footgun, if we are adding a new structural element to the IR, it should be handled by the verifier infra, and not be left to an interface, as it would be too easy for a token type to fall through the cracks (ie. accidentally not adding that the op shouldn’t accept tokens). Consequently, we should add a OpTrait::AcceptsTokens.

Is this really desired? What about a recursive side-effecting operation with control-flow? For example, a switch with all pure ops and nobody consuming results.

I have a slight concern of introducing infra without having an agreed implementation for early-exit (the primary motivation), otherwise we’ll end up introducing code, then move to early-exit and maybe realize the tokens didn’t cut it.

6

In my experience, verifying this kind of static information cannot be done by a simple verifier, it requires at the very least dataflow which I’d argue is a no go. Let me give you an example that shares similarities.

In the current project I’m working, I have a type to represent a definite but yet unnumbered register !amdgcn.vgpr<?> (this is like a memory reference, and it doesn’t have value semantics).

%val0 = alloca : !amdgcn.vgpr<?>
// ...
// something produces %val1
// ...
%rand = func.func @rand() : () -> i1
cf.cond_br %rand, ^bb1(%val0 : !amdgcn.vgpr<?>), ^bb1(%val1 : !amdgcn.vgpr<?>)
^bb1(%arg : !amdgcn.vgpr<?>):

// Point 0:
amdgcn.v_add_u32 %dst, %arg, %rhs : !amdgcn.vgpr<?>, !amdgcn.vgpr<?>, !amdgcn.vgpr<?>

The only way the above code is valid is if for all possible paths the value reaching %arg refers to the same register reference. That is, that after register allocation you get type(val0) == !amdgcn.vgpr<1> and type(val1) == !amdgcn.vgpr<1>.

7

I was referring to the verifier infra here. Each op interface can define a verifier that automatically applies to all ops that implement the interface.

Note, this doesn’t give you the same level of verification. An op trait would not specify which of the potentially many operands is a token.

Tokens are SSA values, so we should be able to reuse existing verification mechanisms. (We don’t have an OpTrait::AcceptsFloats. Type constraints on operands give you full verification.)

Note, Options 5.1 - 5.3 are mutually exclusive options.

IMO, 5.2 is not the ideal solution, for the reason that you described. I was advocating for Option 5.3 here.

@mehdi_amini asked to separate these concerns. I feel like we are mostly aligned on using tokens for early-exit at this point, and it’s mentioned as one of the uses cases for this RFC. If you see some design aspect that wouldn’t fit with early-exit, please comment on this RFC.

8

I was arguing for a change in the verifier infra here: llvm-project/mlir/lib/IR/Verifier.cpp at main · llvm/llvm-project · GitHub . In particular, if the op doesn’t posses the OpTrait::AcceptsTokens, it would automatically emit an error.
If an interface like RegionBranchOpInterface wants to restrict the type further that’s up to the interface. But there should be structural verification of these tokens in core.

I’m not arguing against early-exit with tokens. My concern is, without a draft impl of early-exit with tokens, we won’t know what works and what doesn’t, so landing it without even a proof-of-concept seems risky to me.

9

You’re mentioning “rejecting it in verifiers” as a solution, but that’s exactly the point! Doing so implies making some the generic transformations illegal.
This is the whole point: today if you really need a static connection between two operations, we don’t have any generic way of doing this. You can emulate it in your own pipeline of course, but that’s not meshing into the tools and utilities provided upstream.

I think you missed the part about ODS changes: only ops that opt-in will accept tokens. Any existing op won’t.

I don’t know why the interfaces verifiers are mentioned in the proposal, this is not necessarily and seems redundant with the ODS verifier as far as I can tell.

Honestly I don’t quite see the concern, if you can articulate more specifically a problem you can see specifically let’s address it, but otherwise this seems all quite straightforward to me.

10

From the RFC it’s not clear, @matthias-springer, @mehdi_amini:

  • Is Verifier.cpp doing the verification work, or is it an interface?
  • Is CallOpInterface, FuncOpInterface, …, getting updated, or since they don’t declare token usage means they will reject tokens? ie. more explicitly, is rejecting tokens the default?

It’s a mild concern, I see how tokens will solve the issue, and how they fit. However, until I see the impl working I won’t be confident about the approach, specially around data-flow and possible limitations. Also, I would prefer some questions answered around on the control-flow area first. For example:

  • Can tokens as they are currently proposed model goto? (this doesn’t mean we’ll model goto or generic control-flow). ie, are they future proof.
  • If they can model almost any control-flow, are we considering removing BlockOperands? Why or why not?

These don’t have to be answered yet, and shouldn’t be considered as downvotes (I’m generally in favor of the proposal), as I see them working for the current use-case. But, I’d be great if we could answer the above questions in advance.

11

Re verification. There is also this part:

The change of AnyType to exclude tokens is the main thing. The verification as part of CallOpInterface etc. could be in addition to that (to account for ops that were not defined with ODS), but given that practically all ops are defined in ODS it may not be needed at all.

You can already model goto with unstructured control flow (cf.br). You don’t need tokens for that. (And I think they wouldn’t help with that.)

A block operand is a pointer to a block. A token (as defined in this RFC) is a pointer to an operation or a region. (But not a block.) Tokens would appear only as OpResults or entry block arguments. (A token as a non-entry block argument does not make sense because you would have to to pass the token via cf.br etc., which is forbidden.)

So my answer to this question would be “no”.

Data flow is tricky. But I think this is regardless of whether we use tokens, labels, numbers or any other representation. We will have to think about how to extend the RegionBranchOpInterface.

12

Neither: the ODS change I was referring is to have the definition of AnyType exclude tokens to ensure that no operation today would accept them. A new predicate AnyTypeOrToken would replace AnyType to make the opt-in explicit.

13

Agree. Op verifiers shouldn’t be looking beyond the op and so such verifiers become passes, and those can be easily skipped (even unintentionally). Moving that logic to the type system makes it easier to verify at the op level:

  • Op has a valid token
  • Token points to a valid producer type

Did you scan all such type definitions to see if there’s any other that we need to be careful? IIRC, most of the other Any* are closed world (list of possible values), so not an issue.

The key problem with this proposal for me is that the token type is being described as a generic token type, but discussed with the semantics of control flow. This is what’s getting into people’s heads about GOTO, basic blocks, etc.

As I said in the document, I think we need to make clear the separation between the builtin token type and its early-exit SCF usage.

14

AnyType is the only one that I found. I think this should do: [mlir][IR] Add builtin `TokenTypeInterface` by matthias-springer · Pull Request #195640 · llvm/llvm-project · GitHub.

15

Can you expand a bit on that part? Do you need to attach extra parameters to the token type? What’s the benefit of distinguishing between CF tokens and other tokens in the type system?

16

Let’s say we have two different token semantics A, and B, eg. control-flow and LLVM token. How does an op that only accepts tokens of B semantics rejects tokens with A semantics?

As it stands with an opaque token types, ops would need to inspect directly the producing entity just to reject the incorrect semantics. If it’s an interface then the token can signal a promise around what the token producing entity offers, consequently, ops can locally verify that it’s the right kind. That is, terminators will explicitly request CFTokenType and reject LLVM tokens.

17

There aren’t multiple possible semantics in the current definition of what a Token is. The token is an opaque value without any semantics. Think of the whole thing at only providing a link between two operations: a fixed def-use chain that can’t be altered (there may be caveat: it’s not clear if it can be a bi-directional link or not, it has consequences on CSE/OperationEquivalent modeling).
So there is no “control flow semantics” or “LLVM Token semantics” in consideration here.

Right: this is the intended way to handle it. The token is just here to provide direct access to the producing entity, and guarantee that you can get it (which is the usually frown upon “verifier looking through use-def chain” pattern).

18

I interpreted @fabianmc comment differently. Let me try to expand…

The token itself doesn’t have semantics, but ops that use them imbue with a particular semantics. I think the concern here is to know what happens when two different usages collide (due to a bug in the compiler).

For example:

  // Dialect one, semantics A (token has no semantics, the op does)
  %0, %t0 = d1.create_link %a, %b : ty, ty -> ty, token
  ...
  d1.consume_link %t0 : token -> ()

  // Dialect two, semantics B (token still doesn't have semantics...)
  %3 = d2.create_link : token
  ...
  %4 = d2.consume_link %x, %y, %0 : ty, ty, token -> ty // Compile bug, should be %3

Without knowing what kind of token I’m expecting, it’s hard for the op to verify that the token received in d2.consume_link is the expected one (%3 and not %0).

The only way to verify correctness of semantics for those ops is to limit the scope on the token producers. In the example above, d2.consume_token can verify that the producer of the token belongs to dialect d2 or is exclusively produced by d2.create_link, which is still in the purview of the op verifier, so it’s not totally unexpected.

IIUC, Fabian’s point is that having a builtin interface instead, would allow both d1 and d2 to create their own token types, which implement the token interface, and then verification would be trivial.

From what I understood of the original proposal, that may not be necessary, given that you can already verify producers (usually a small list, so no high verification costs), and the semantics A or B would still remain on the operations themselves, not the token type.

@fabianmc does that address your concern?

19

Looking into it again I guess I would lean now to Type solution not to pay Interface cost everywhere.

To satisfy verification one can always add their custom traits MyTokenProducer and MyTokenConsumer that verifies proper origin of consumer tokens.

20

Looking for reviews: I prepared two pull requests to add a builtin token type.

In particular, I’d like to draw your attention to the documentation in Tokens.md. That’s the main part of the pull request. Please comment and/or suggest changes if the wording is unclear or something is missing.