PaperlayerView exact revision on arXiv

Source-linked AI summary

Coexponential Exploration in the Clef Programming Language

Houston Haynes

arXiv:2610.12911v1cs.PLcs.DCcs.LO

TL;DR

Well-typed concurrent services can still misroute replies, deadlock, or leave remote state changing after a caller times out. Clef retains continuations and ownership dependencies, with conditional preservation for actor translation and a terminating finite communication summary that over-approximates abstracted traces.

  • Problem

    Well-typed operations can still misroute replies, wait indefinitely, or allow remote state changes after a caller times out.

    Source: §1 · p. 1

  • Method

    Clef translates actor suspension into continuation frames under local step contracts and summarizes blocking-call dependencies as a finite wait relation.

    Source: §4.2 · p. 8, §5.2 · p. 11

  • Results

    The finite communication-summary construction terminates and includes every finite concrete communication trace after abstraction to declared tags and roles.

    Source: §5.1 · p. 10

  • Takeaways & Limitations

    Retained dependencies let edits revisit affected applications and lowering scopes while reusing stable evidence, reducing repeated checking and compilation.

    Source: §10.7 · p. 28

    A cycle in the conservative wait summary may reflect mutually exclusive paths, so it is a candidate for refinement or a protocol argument.

    Source: §5.2 · p. 11

Abstract

from arXiv · show

Clef was created as a concurrent programming language whose compiler tracks state ownership, waiting computations and request dependencies. We develop a coexponential account of stateful services and their client pools within this design. Delimited continuations retain the computation and resources needed to complete each interaction. These structures give our compiler premises for verifying service composition and preserving it through native lowering to multiple hardware targets. We connect finite actor state transitions to the initial, service and final rules of a coexponential server. A separate operational account relates actor dispatch to single-use continuation frames. We prove state-ownership and reply preservation for that translation, give a finite communication-summary analysis, and circular-wait exclusion from the conditions needed. A further result identifies when changing service order preserves both state and replies. Our Program Semantic Graph retains these facts through compilation. We are researching reusable proofs to confirm the ownership and communication interfaces, while our BAREWire implementation connects message meaning to its unboxed representation across respective endpoints. A distributed worker example preserves request identity across suspension, reordered replies and boundary conversion. Urschel's elimination-growth bounds supply quantitative premises for a solver service, whose accuracy and failure budget compose with the protocol contract. The design we envision connects automatic structural analysis, reusable proof terms and native realization. Protocols determine the admissible interactions, continuations expose their storage requirements, and retained dependencies support differential compilation. Developers can express ordinary stateful services while the compiler carries the conditions for their correct composition across execution targets.

1. Concurrent Composition in Clef

Clef makes ownership, communication, and waiting dependencies explicit so the compiler can check how stateful services compose. The paper connects coexponential service pools to actor operations and retains their relationships through compilation.

1. Concurrent Composition in Clef

  • Well-typed operations can still misroute replies, wait indefinitely, or let a remote request change state after its caller times out.These failures concern relationships between operations, not just their input and output types or freedom from data races.Source: §1 · p. 1
  • The compiler account makes the construction available through ordinary service interfaces while carrying resource, protocol, and dependency information for composition checks.This connects the coexponential construction to Clef’s native compilation and automatic verification design.Source: §1 · p. 2, §1.1 · p. 2

1.1 Stateful Service as a Type-Theoretic Construction

  • Coexponentials express a shared stateful service and its client pool, which the paper connects to actor behavior and the compiler’s continuation representation.Delimited continuations retain the control and resources of a suspended interaction.Source: §1.1 · p. 2
  • Reusable proofs for ownership, reliable channels, and commuting updates can be applied where program values and operations satisfy their premises.The compiler connects applicable proof terms to those program sites.Source: §1.1 · p. 2

1.2 Retaining the Relationships Through Compilation

  • The Program Semantic Graph retains source identities, control, resources, and communication relationships, including joint obligations linking a reply to its invocation and suspended continuation.Later transformations can use those retained relationships to establish that they still realize the same interaction.Source: §1.2 · pp. 2–3

2. A Service and Its Clients

A service pool models multiple clients sharing an evolving private state, with each selected handler replying to its client. Coexponential rules describe the pool and server, while service order and runtime policy determine which interactions occur.

2. A Service and Its Clients

  • A stateful service must account for repeated requests that share evolving state, not only one function application.The client pool shares one service; handlers transform its private state and reply to their clients, and finalization consumes that state.Source: §2 · p. 3, Figure 1 · p. 3
  • The server coexponential and client-side pool use dual views of one interaction, with clients following the protocol dual to the server’s view.The connected pool has type Pool(A⊥).Source: §2 · pp. 3–4

2.1 The List Presentation

  • The list presentation forms a pool from an empty pool or a client plus the remaining pool, and lets the server finalize or serve while retaining the service.Initialization provides the internal state protocol, each worker consumes the previous state and provides the next, and finalization consumes the state.Source: §2.1 · p. 4
  • The server rule’s initialization, worker, and finalization premises give an actor arrangement a precise construction, with declared state values and a session representation for transferring state.Replies and finalization may also export values specified by the interaction protocol.Source: §2.1 · p. 4

2.2 Service Order and Observable Results

  • Pool formation permits different client orders, and those orders can produce different results even for a valid session.Runtime policies such as FIFO can restrict the orders admitted by the pool; applications requiring identical answers across orders need an additional condition.Source: §2.2 · p. 4
  • An indefinitely available service needs admission, resource, and scheduling contracts beyond the fixed-point interface for a finite client batch.Those contracts determine how the persistent interface is realized on a bounded machine.Source: §2.2 · pp. 4–5

3. Constructing an Actor Service

The paper constructs a coexponential server for finite actor transitions, then extends the construction to practical value representations and parameterized computations. Its worker derivation connects each request to the specified reply and successor state.

3. Constructing an Actor Service

  • The construction generalizes a Boolean compare-and-set example to finite state, payload, and reply sets and a family of message tags.The state declaration supplies the state set, its encoding supplies the internal protocol, and the handler realization supplies the worker premise.Source: §3 · p. 5, §3.1 · p. 6

3.1 From Values to an Internal Protocol

  • For every family of total finite-state actor transitions, the worker derivation returns the specified reply and successor state, and a coexponential server matches each selected finite client order’s state sequence and labelled replies.The construction assumes a specified initial state and a nonreentrant discipline in which one handler owns the actor state until it returns its successor state, including while suspended.Source: §3.1 · p. 5, §3 · p. 5

3.2 A Practical Representation Interface

  • Typed provider and consumer operations let machine representations reuse established communication and value-preservation laws instead of enumerating every possible word value.The compiler checks the actual parameters and participants of reusable representation and handler proofs.Source: §3.2 · p. 6

3.3 Parameters, State and Compositional Structure

  • Parameterized computations relate a configuration space to an input-output computation, while a compatible reparameterization compares computations through a map between configuration spaces.A diagonal map can express two component uses drawing on one configuration, whose shared origin must be preserved in storage and update behavior.Source: §3.3 · pp. 6–7
  • The parameterized algebra does not by itself compare operational realizations; the compiler uses a separate two-category construction to apply permitted transformations when participants meet their premises.Developers continue to work with the handler’s data and operations.Source: §3.3 · p. 7

4. Executing the Protocol with Delimited Continuations

Delimited continuations retain a suspended interaction’s live values, return point, and owned resources while connecting actor execution to a coexponential service. The translation carries conditional state-ownership and reply-preservation guarantees, with storage, completion, and demand behavior tied to the computation’s needs.

4. Executing the Protocol with Delimited Continuations

  • Delimited continuations represent a handler’s bounded remainder, retaining its live values and return point within an identified control scope.The coexponential describes the persistent service and its clients; the continuation realizes control within a particular interaction.Source: §4 · p. 7

4.1 The Retained Frame

  • Suspension moves the handler’s live frame and exclusive state into a continuation; further mailbox dispatch for that actor waits until its state returns.Libraries permitting additional same-actor interleaving need a corresponding state-sharing invariant.Source: §4 · p. 7, §4.1 · pp. 7–8

4.2 Local Preservation

  • Under the transition-primitives contracts, the translation preserves unique actor-state ownership and at-most-once completion, with matching visible request, reply, and state events in both directions.Administrative target steps preserve the relation and finish in finitely many steps.Source: §4.2 · p. 8

4.3 Completion, Failure and Storage

  • A reply-timeout race atomically selects one outcome and resumes once; timeout ends only the local wait, while remote effects and cleanup remain governed by the remote protocol.Late messages retain invocation and generation identities so the receiver can reject them after the completion right is consumed.Source: §4.3 · p. 9

4.4 Captures, Demand and Delivery

  • The Program Semantic Graph binds reusable laws to operations and captured values, supporting justified optimizations and resource transfers across demand, sharing, and resumption.It records live values and backing-storage lifetimes across suspension cuts; incremental reuse accounts for actual reads and effects.Source: §4.4 · pp. 9–10, §4.3 · p. 9

5. Recovering Communication Structure

Clef recovers finite communication summaries from handler control flow and records possible blocking dependencies. Under stated coverage and progress conditions, these analyses support protocol checks, exclude represented wait cycles, and establish completion for finite batches.

5.1 A Finite Summary with a Stated Guarantee

  • For the stated finite-control fragment, the communication automaton construction terminates and includes every concrete communication trace after values and endpoint instances are abstracted to declared tags and roles.Its cost is a traversal of the expanded graph plus emitted alternatives.Source: §5.1 · pp. 10–11

5.2 Wait Dependencies

  • If every actual blocking dependency is included in W and the natural-number rank decreases along each edge, no execution has a circular wait consisting of those dependencies.Conservative summaries can contain cycles from mutually exclusive paths, requiring refinement or a protocol argument.Source: §5.2 · p. 11

5.3 What Makes a Request Complete

  • For a finite batch, acyclic dependencies support completion when local work terminates, dependency spawning is finite, ready work is fairly scheduled, and required terminal outcomes are eventually delivered.Request-selection fairness prevents a queued request from being starved.Source: §5.3 · pp. 11–12

6. When Service Order Can Change

Service order can change both state and client-visible replies, so reordering requires conditions on computations and observations. The section states a pairwise condition for permutation-invariant outcomes and relates dependency structure to compilation placement.

6.1 State and Labelled Replies

  • For every pair and reachable intermediate state, the stated equations make all service permutations yield the same final state and request-indexed reply map.The condition preserves both state and the reply associated with each request occurrence.Source: §6.1 · p. 12
  • State agreement alone is insufficient: incrementing a counter can commute as an update while returning different replies to clients.The compiler can retain the valid state law without using it to justify a stronger client-visible equivalence.Source: §6.1 · pp. 12–13
  • Independent workers can fill distinct result-map slots in either arrival order when their acknowledgements remain unchanged by the other update.A later computation reads the result map under its own combination rule.Source: §6.1 · p. 13

6.2 Dependency Width and Placement

  • Dependency width is the largest set of pairwise incomparable events in a finite acyclic dependency graph, and equals the minimum chain-cover size.Chains describe ordered work; antichains identify work unconstrained by the retained relation.Source: §6.2 · p. 13
  • Placement must also account for readiness, target capacity, and event resources; pending requests alone do not prove handlers can run simultaneously.The coordinator example constructs both worker requests before either result is available, then waits for both replies.Source: §6.2 · p. 13

7. Proofs at the Communication Boundary

The communication-boundary account connects message transfer to ownership and protocol proofs, then relates unreliable transport and native representations to the values and resources received. These boundary contracts compose with the waiting continuation.

7. Proofs at the Communication Boundary

  • A communication binding connects actual memory and transport operations to a justified account of what becomes available when a request is accepted.The binding corresponds Clef operations to reusable ownership, protocol, and distributed reasoning.Source: §7 · p. 13

7.1 A Message Can Transfer a Proof Resource

  • Protocol send and receive steps transfer message assertions while advancing endpoint protocols, and a handler can retain its reply endpoint while establishing its postcondition.A suspended handler's frame retains these assertions until resumption restores them.Source: §7.1 · pp. 13–14
  • Exclusive reply authority supports at-most-once use, but eventual reply additionally requires a completion argument because affine resources may go unused.The communication proof establishes resource-safe steps; the progress contract supplies conditions for those steps to occur.Source: §7.1 · p. 14

7.2 From Reliable Channels to an Unreliable Network

  • A duplicated packet can carry a duplicable indexed witness without duplicating logical ownership, because the receiver's exclusive protocol state releases the resource once.The protocol index and invocation identity survive encoding and decoding, allowing results to match their intended outstanding requests.Source: §7.2 · p. 15
  • Verified channel specifications establish partial correctness; completion claims also depend on target delivery, connection-lifetime, and failure premises.The compiler records these premises with the selected channel instance.Source: §7.2 · p. 15

7.3 BAREWire and the Received Meaning

  • BAREWire composes encoder, communication-library, and decoder obligations so the received value and resource assertion correspond to the same invocation and interpretation.Exact mappings require valid tags, covered widths, initialized ranges, endpoint identifiers, and referenced-storage lifetimes.Source: §7.3 · p. 15

7.4 Composing Exact Representations

  • Checked round trips make admitted representation conversions compose as a groupoid, but a native operation also needs a law connecting its encoded implementation to the source computation.When precision changes, the boundary instead carries its stated value relation and error bound.Source: §7.4 · p. 16

8. A Distributed Request from Admission to Completion

The distributed example tracks identified tasks and their outstanding replies through coordinator suspension, worker execution, and local or remote placement. Its contracts preserve the relationship between each request, result, and continuation.

8. A Distributed Request from Admission to Completion

  • The coordinator divides one client calculation into two named worker tasks and combines their results, while each worker owns its state and follows an admitted protocol.The coordinator's composition proof covers its pending requests and endpoints.Source: §8 · p. 16

8.1 Identities and Outstanding Work

  • Fresh job, generation, and task identities bind each request to an immutable input version; single acceptance consumes its authority, rejecting duplicate bytes and stale-generation replies.Distinct task updates commute when they write separate result slots, making the result map independent of reply arrival order.Source: §8.1 · p. 17

8.2 Suspension and Wait Structure

  • The coordinator can issue both requests before awaiting results, and its retained frame holds task state, outstanding endpoints, and authority to reply to the client.The rank certificate and pending-set invariant address different failures; the continuation preserves both the invariant state and the code consuming the next result.Source: §8.2 · p. 17, Figure 2 · p. 18

8.3 Location Transparency and Direct Communication

  • A location-transparent reference separates service identity and protocol from placement, while each invocation keeps its endpoint, reply identity, and caller continuation across local or remote bindings.Each placement supplies its own admission, ordering, delivery, and failure premises.Source: §8.3 · p. 18
  • For the two-task example, frame extent, queue admission, and reply capacity can be checked before execution; variable client counts require an admission bound or resource invariant.A placement refinement must relate accepted requests, state transitions, and replies to those of the source service.Source: §8.3 · pp. 18–19

9. A Solver Service with a Quantitative Contract

The solver example uses an elimination-growth bound to inform worker arithmetic choices, while protocol and boundary contracts carry task results into a distributed join. The accuracy result applies to completed outputs under stated task and error assumptions.

9.1 A Growth Bound as a Worker Premise

  • Urschel's elimination-growth result informs candidate factor ranges and arithmetic configuration, while the realized algorithm and residual contract establish returned accuracy.The worker protocol carries success or failure as a typed outcome.Source: §9.1 · pp. 19–20

9.2 Accuracy at the Completed Join

  • For a finite admitted task set, exact task identification and single acceptance at the join support an accuracy bound for a completed distributed result.The proof bounds reduction error by the worker, boundary, and reduction error contributions, then uses a union bound for bad-success events.Source: §9.2 · p. 20
  • The accuracy bound concerns completed inaccurate outputs, while completion itself depends on separate premises supplied by the protocol.A retry policy must record attempts and sampling assumptions; reusing a sample after observing its outcome needs a conditional argument.Source: §9.2 · p. 20
  • The quantitative proof makes a worker result useful to an application with an explicit accuracy requirement by connecting it to the waiting computation.The coexponential protocol describes the worker interaction, while continuation and network proofs connect the result to its caller.Source: §9.2 · p. 20

10. Keeping the Proofs Useful to the Compiler

This section examines how the compiler retains continuations, static facts, and proof dependencies to constrain execution and support proof composition, transport across compilation stages, and native realization. It also develops selective recompilation, including the conditions under which a checked same-interface replacement transports safety while unaffected evidence remains valid.

10.1 Four Tiers and Their Interfaces

  • The four verification tiers move from structural inference and generated local checks to reusable proofs and relational guarantees, with higher tiers reusing facts established about the same program.Tiers 1–3 derive application parameters from source and graph structure; library authors provide general lemmas and bindings, while project annotations can select Tier 4 relations. Proof interfaces state what judgments they accept and produce; the design does not claim cut elimination for a new combined fixed-point calculus.Source: §10.1 · p. 21

10.2 Composing Components and Their Refinements

  • Contextual refinements form a strict locally preordered two-category in which successive and interface-compatible component refinements compose.A component comparison concerns finite observable behavior; completion or probability guarantees retain their own admitted judgments and premises, such as scheduler fairness assumptions.Source: §10.2 · pp. 22–23

10.3 Evidence Across Compilation and Reasoning Modes

  • Coherent transport keeps evidence applicable across lowering and reasoning modes, so a reusable fact remains tied to the operation and premises that justify its use.The compilation-sheaf account says checking compatibility on immediate cover edges suffices for longer stage chains; preservation contracts connect stage descriptions to generated operations, while joint constraints retain shared identities and aggregate resource predicates.Source: §10.3 · pp. 23–24

10.4 From a Frame to Native Operations

  • The compiler selects native realizations when an exact codec establishes value interpretation, contextual refinement admits replacement, and coherent proof transport connects facts to consuming operations.Baker constructs semantic relationships and obligations, Alex witnesses settled consequences in portable MLIR, and Composer's backends realize operations for targets.Source: §10.4 · p. 24

10.5 Stateful Services Across Processor Classes

  • Across processor classes, target contracts preserve service state transitions and labelled replies while governing ownership, placement, and continuation storage.SIMD and SIMT work can divide disjoint outputs among lanes or threads and reassemble ownership before publishing successor state; GPU synchronization and asynchronous completion remain obligations. Tiled NPU execution retains request identity and transfer dependencies, while FPGA circuits must preserve state and reply relationships through pipelining, admission, backpressure, and reset.Source: §10.5 · pp. 25–26
  • A single-core MCU can run concurrent services while awaiting device events, with effectful MMIO operations, interrupt continuations, and frame and resource bounds preserved.The account supports device-oriented unikernels using the same service, continuation, and ownership model as hosted distributed applications.Source: §10.6 · p. 26, §10.5 · p. 26

10.6 Execution, Supervision and Scheduling

  • Ariel resumes ready worker continuations, while Prospero governs placement, lifecycle, and recovery and Olivier executes workers with owned state and resources.Actor-state authority persists across suspension; budget exhaustion can trigger retirement, restart with a fresh arena, or fault escalation. Supervisory execution depends on reserved control-plane capacity, and progress relies on dispatch and delivery assumptions.Source: §10.6 · pp. 26–27
  • On the single-core unikernel profile, a retained continuation frame serves as the task and dispatch point, while asynchronous resource use constrains safe retirement and storage reclamation.Admission, identity retirement and storage reclamation are separate: outstanding device or foreign use must complete, or a target-specific revocation guarantee must end access.Source: §10.6 · p. 27

10.7 Differential Compilation

  • Differential compilation follows changed premises through proofs, layouts, interpretations and lowered artifacts, retaining fragments only when their supporting assumptions and exposed contract remain valid.A Huet zipper focuses graph traversal and records context [7]; changed reply representations, call targets or solver settings affect their dependent components.Source: §10.7 · pp. 27–28
  • Under the stated realization and coherence conditions, a checked same-interface replacement preserves the transported safety judgment in the realized target and retains unaffected evidence.Affected records are re-established and recomposed with retained records; certificates bound to the previous artifact are rebound or reconstructed.Source: §10.7 · p. 28
  • Reusable library proofs and stable evidence outside the dependency closure reduce repeated checking and compilation while preserving why each fragment was admitted.Per-cut liveness reduces retained frame data, established ranges justify representations, and dependency-directed revalidation limits repeated proof construction and lowering to affected scopes.Source: §10.7 · pp. 28–29

11. Relationship to Established Work

The paper situates its service and continuation account among work on session calculi, executable languages, distributed verification, and control. It distinguishes what those precedents establish from the operational and ownership obligations addressed here.

11. Relationship to Established Work

  • Session calculi, delimited control, and separation logic contribute distinct proof responsibilities, whose premises should remain explicit when combined.The paper uses compilation stages to connect their results without erasing their separate obligations.Source: §11 · p. 29

11.1 Stateful Sessions and Progress

  • CSLL preservation and progress support the service construction, while actor correspondence, fair termination, and request completion retain separate operational or runtime obligations.Actris and LinearActris address channel safety and global progress; completion of each admitted request requires additional premises.Source: §11.1 · p. 29

11.2 Reconstruction and Distributed Verification

  • The finite communication analysis addresses a defined extraction problem and connects inferred session shapes to the wait relation, captured frames, and their actual send or receive operations.The authors position this alongside existing inference and automata-synthesis work, while retaining the fragment each procedure covers.Source: §11.2 · p. 30

11.3 Computation, Control and Logical Duality

  • The paper distinguishes its session modality from categorical coexponentials dual to function types, and its continuation proof from separate resource interpretations and adaptive-service applications.Each imported interpretation retains its own typing and operational obligations.Source: §11.3 · p. 30

12. Stateful Services in a Concurrent Language

The paper connects stateful services and client pools to explicit actor protocols, continuations, and distributed proof infrastructure. These structures support inspectable reasoning about message meaning, representation, and compilation across execution targets.

12. Stateful Services in a Concurrent Language

  • The coexponential construction, finite actor translation, and continuation account jointly track protocol, state, resources, and reply authority across suspension.Wait analysis, scheduling assumptions, and application-specific laws remain conditions for completion and order changes.Source: §12 · p. 30
  • Across machine boundaries, admitted protocol steps preserve resource assertions, indexed acceptance guards against duplicated ownership, and BAREWire connects messages to their received meanings.The solver example combines request identity and resources with Urschel's growth bound and a quantitative worker contract.Source: §12 · p. 31
  • Parameterized composition, realization comparisons, mode interfaces, and compatible stage evidence retain a chain of justification from source request through native completion.This chain connects the suspended continuation and its realization across representation changes.Source: §12 · p. 31
  • The compiler is described as supporting device-bound, vector, GPU, tiled, spatial, and distributed execution, while checking affected contracts and retaining surviving work after changes.The paper presents this as a concrete concurrent application of its compiler mechanisms.Source: §12 · p. 31

Software Availability

The paper identifies public source repositories and documentation for Clef and its supporting framework. It states that component licensing terms are provided in each repository.

Software Availability

  • The Clef language, Composer compiler, and supporting libraries are developed under the Fidelity Framework project, with source repositories available on GitHub.The passage gives the repository address as https://github.com/FidelityFramework.Source: Software Availability · p. 31
  • The language specification, design rationale, and compiler documentation are published at clef-lang.com, and component license terms are detailed in each repository.The compiler connects these components through the paper's obligation and preservation interfaces.Source: Software Availability · p. 31
Loading 2610.12911v1…