guard obhash_guard(key: ObKey)struct ObjectHeader {kei oid: OID;key ty: ObType;region hash guarded_by obhash_guard(ObKey(ty, oid)) {next: *ObjectHeader;}}
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMN8y-NnVDPCKm%3Dqyh2O3NGx2ckMdi19VXeLP566Y2LTA%40mail.gmail.com.
In the course of a design "chat" with an LLM today, a potentially interesting "how should these interact" question emerged. Still working through it, but I want to sketch it here in case it sparks adjacent useful thoughts. In this note, I'm talking in the PL context, not the OS context, though I'll pull some explanations from the Coyotos kernel.I don't recall that we've talked much about capabilities in the context of concurrency guards. It seems to me that this has some of the flavor of split capabilities as follows:
- "Opening" a capability establishes [selected] access to the region guarded by the capability.
- "Opening" a mutex establishes me non-interference over the region guarded by the mutex.
- The intersection of these regions is where permission and concurrency safety is assured.
- Up to a point, a compiler can check this intersection and enforce the two safety requirements.
So three questions here:First, is our framing of capabilities as (permission, object) correct? Would it be more accurate to characterize a capability as (permission, region), where (at the byte level) the reachable region may have a complex shape governed by various forms of guard-like concepts, further governed by guard lifetimes, and still further governed by temporary immutability requirements on any data structure contents used to derive the relation between a guard structure and its dominated region [see below]?
Second, it seems a little interesting (though I think this is probably an artifact of our particular use cases) that many mutex regions are not scoped by a single object. For example., when objects are on an internally threaded list, the list mutex region involves all of the member pointers across all of the participating objects (or a subset of these, e.g. hash table chain pointers).
Third: correct mutex management is almost always scoped by hierarchical control flow, because this guarantees release ordering and prevents dangling held mutexes. Because of this, it is usually true that AcquiredRegion variables can be "lifted" to effect variables and passed implicitly (i.e. as compiler-introduced effect variables). In capability terms, does this make them ambient, or does it merely open up a new way of expressing the thing that a capability structure captures? From a practical programming perspective, carrying acquired regions around explicitly can rapidly have you carrying 40 or 50 bookkeeping variables that entirely obscure the program's meaning.
I am explicitly suggesting that regions are a lot richer than our most common shorthand understanding of objects, and that this is useful.
To understand what I mean by guard/region relation, consider an object hash table. In low-level systems, the link pointers often want to reside in the objects, so you end up with a relation that might look like:guard obhash_guard(key: ObKey)struct ObjectHeader {kei oid: OID;key ty: ObType;region hash guarded_by obhash_guard(ObKey(ty, oid)) {next: *ObjectHeader;}}where obhash_guard() is a pure, deterministic function of its arguments. In a stateful language, the values of ty and oid must remain stable while the hash region remains acquired.There is a further interesting outcome given the Coyotos transaction and mutex auto-release discipline, which is that the effects associated with auto-released mutexes are monotonic. That is: the regions opened only increase as the transaction proceeds and are all instantaneously whacked by end-of-transaction. We need to partition these from the few manually managed regions, but that doesn't seem difficult.I had been reaching for a way to express this kind of thing in BitC for many years. I find myself of two minds here:
- This looks like a useful starting point, and the introduction of guard relation functions feels like 80% of what I couldn't pin down. I wish I'd known about the Java guarded_by work much sooner!
- This is syntactically too cumbersome for general purpose programs, though it feels syntactically as if it can be simplified a bunch for the common use cases (as, e.g., Rust does).
- Nonetheless, the place to start for investigation is with a syntax that is more explicit rather than less.
- Purity and init-only are powerful here, because init-once immutable objects obviously don't need guards at all.
- There are some entertaining implications for library design here.
Jonathan
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMN8y-NnVDPCKm%3Dqyh2O3NGx2ckMdi19VXeLP566Y2LTA%40mail.gmail.com.
A capability to a region seems to rhyme with a certificate delegation to a set of objects, such as *.mp3. That certificate is not a capability because it does not designate a resource. (There's no "object" that is the set.) You must create a capability (a delegation to a specific object) before you can invoke that object.Is that what you're talking about?
On Sun, May 24, 2026 at 10:46 AM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:In the course of a design "chat" with an LLM today, a potentially interesting "how should these interact" question emerged. Still working through it, but I want to sketch it here in case it sparks adjacent useful thoughts. In this note, I'm talking in the PL context, not the OS context, though I'll pull some explanations from the Coyotos kernel.I don't recall that we've talked much about capabilities in the context of concurrency guards. It seems to me that this has some of the flavor of split capabilities as follows:
- "Opening" a capability establishes [selected] access to the region guarded by the capability.
- "Opening" a mutex establishes me non-interference over the region guarded by the mutex.
- The intersection of these regions is where permission and concurrency safety is assured.
- Up to a point, a compiler can check this intersection and enforce the two safety requirements.
1) What's the relationship with split capabilities? I don't see it.
2) This seems very close to reference capabilities. There is no one canonical reference capability system, rather it is a family, including both Pony and Rust. Pony also has ocaps. Do the rules you have in mind fall within the reference capability framing?
3) Just btw, E represents a different but related cross over. After all, the subtitle of my dissertation is "Towards a Unified Approach to Access Control and Concurrency Control". This starts with the assumption that mutable objects are stably partitioned into vats. If you assume a shared TCB (which E does not assume) you could combine this with reference caps to move ownership of mutable objects between vats. I think you assume a shared tcb in the relevant sense.
So three questions here:First, is our framing of capabilities as (permission, object) correct? Would it be more accurate to characterize a capability as (permission, region), where (at the byte level) the reachable region may have a complex shape governed by various forms of guard-like concepts, further governed by guard lifetimes, and still further governed by temporary immutability requirements on any data structure contents used to derive the relation between a guard structure and its dominated region [see below]?They are both correct. For most purposes, the framing as (permission, object) is the more important one.
Third: correct mutex management is almost always scoped by hierarchical control flow, because this guarantees release ordering and prevents dangling held mutexes. Because of this, it is usually true that AcquiredRegion variables can be "lifted" to effect variables and passed implicitly (i.e. as compiler-introduced effect variables). In capability terms, does this make them ambient, or does it merely open up a new way of expressing the thing that a capability structure captures? From a practical programming perspective, carrying acquired regions around explicitly can rapidly have you carrying 40 or 50 bookkeeping variables that entirely obscure the program's meaning.That's one of many reasons that traditional mutexes are a bad idea. E is naturally deadlock-free for other reasons.
On Sun, May 24, 2026 at 2:25 PM Mark S. Miller <eri...@gmail.com> wrote:On Sun, May 24, 2026 at 10:46 AM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:In the course of a design "chat" with an LLM today, a potentially interesting "how should these interact" question emerged. Still working through it, but I want to sketch it here in case it sparks adjacent useful thoughts. In this note, I'm talking in the PL context, not the OS context, though I'll pull some explanations from the Coyotos kernel.I don't recall that we've talked much about capabilities in the context of concurrency guards. It seems to me that this has some of the flavor of split capabilities as follows:
- "Opening" a capability establishes [selected] access to the region guarded by the capability.
- "Opening" a mutex establishes me non-interference over the region guarded by the mutex.
- The intersection of these regions is where permission and concurrency safety is assured.
- Up to a point, a compiler can check this intersection and enforce the two safety requirements.
1) What's the relationship with split capabilities? I don't see it.To manipulate a region in the presence of concurrency, one must have both a capability authorizing the access to the region and a mutex to some region establishing temporal non-interference across CPUs. The two, taken together, convey a guarantee of safe concurrent access to the intersection of the respectively governed regions.It's the intersection part that feels a little like my (now vague) memory of split capabilities. Well, that and the fact that two authorities are being combined that don't necessarily designate the same thing.
2) This seems very close to reference capabilities. There is no one canonical reference capability system, rather it is a family, including both Pony and Rust. Pony also has ocaps. Do the rules you have in mind fall within the reference capability framing?I suppose I'll have to go look and find out. :-) Thanks.3) Just btw, E represents a different but related cross over. After all, the subtitle of my dissertation is "Towards a Unified Approach to Access Control and Concurrency Control". This starts with the assumption that mutable objects are stably partitioned into vats. If you assume a shared TCB (which E does not assume) you could combine this with reference caps to move ownership of mutable objects between vats. I think you assume a shared tcb in the relevant sense.Worse, I'm assuming shared-memory mutable concurrency. The threads are running mutually trusted identical code, but there is still a need to deal with access control and concurrency safety. This is relevant in the context of things like a kernel rather than a high-level distributed system.So three questions here:First, is our framing of capabilities as (permission, object) correct? Would it be more accurate to characterize a capability as (permission, region), where (at the byte level) the reachable region may have a complex shape governed by various forms of guard-like concepts, further governed by guard lifetimes, and still further governed by temporary immutability requirements on any data structure contents used to derive the relation between a guard structure and its dominated region [see below]?They are both correct. For most purposes, the framing as (permission, object) is the more important one.Informally, I'd agree. From a more rigorous perspective, I am contemplating whether suitably typed regions subsume objects.
Third: correct mutex management is almost always scoped by hierarchical control flow, because this guarantees release ordering and prevents dangling held mutexes. Because of this, it is usually true that AcquiredRegion variables can be "lifted" to effect variables and passed implicitly (i.e. as compiler-introduced effect variables). In capability terms, does this make them ambient, or does it merely open up a new way of expressing the thing that a capability structure captures? From a practical programming perspective, carrying acquired regions around explicitly can rapidly have you carrying 40 or 50 bookkeeping variables that entirely obscure the program's meaning.That's one of many reasons that traditional mutexes are a bad idea. E is naturally deadlock-free for other reasons.Some shared concurrent things in the world are stateful. :-) E.g. is it possible to build a high-performance E runtime successfully in E?
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QNA%2B8VeyVy4LoYuRpiqyBVJ4fXpDp2sMPCQ8Z9uS%3DRn9g%40mail.gmail.com.
Sounds to me like normal ocap rights amplification. But now that you point that out, I don't remember enough about split capabilities to comment further. I'll leave that to Alan. Alan?
How do suitably typed regions account for context switching on a call from one encapsulated object to another? If invocation is not part of your model, then it is neither ocaps nor split caps. I refer to such things as "memory capabilities". For example, Tahoe-LAFS is about memory-capabilities. Whether your particular memory-capabilities are a subset of ocap, caps-as-keys, caps-as-rows, or something else depends.
Some shared concurrent things in the world are stateful. :-) E.g. is it possible to build a high-performance E runtime successfully in E?No. But it is in reference capability systems. It might even be in E combined with reference capabilities to enable ownership transfer between vats. Some similar academic experiments seem to be successful. (Before you ask, I would have a hard time finding these experiments.)OTOH, it is impossible to build a high performance distributed invocation system without promise pipelining.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYj0Rk7ZN_s5ZTDqYKeEuZKn-V%2BWiw%2BbouRPy%3DmKqLh-9w%40mail.gmail.com.
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMkzN8F4OHUdAvOgC5Z_uLvcYiabX%3D6gq15Ok6A-v8W2A%40mail.gmail.com.
I've regretted that I can't adapt Cap'N Proto for Coyotos.
I have some of the coyotos idl files translated to capnp (not included - I can add them, though).
I'm a big fan of promise pipelining, but "impossible" is far too strong a claim here. It depends greatly on the nature of the messages being sent, the dynamic dependency structure of the messages, and the promise lifespans required. There's also a question of context for the statement. As good as both are, I'm not aware of any practical realization of promise pipelining in non-GC'd languages, and I'm not aware of any that address denial-of-heap attacks (though I see that throttling is possible). I've regretted that I can't adapt Cap'N Proto for Coyotos.