Replies: 1 comment 2 replies
-
A naturally arising problem out of this is that having named ports exist in the first place (and as a kernel primitive) is that formal verification of all of this becomes more difficult: if we started with model checking, we would have to allow for such things (and to take up some space of names). Even if this were modelled with up to 64 possible names (represented as a 6 bit bit vector), our state space would explode even higher, rather than the simple 1 page read/write sharable content already there, plus interactions with anonymous interfaces to use them. |
Beta Was this translation helpful? Give feedback.
2 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
At a high level, IPC needs to operate with as little interference from the kernel as possible. Poking around for how similar systems have worked, a reasonable implementation appears to be:
A problem now arises: it appears that the only use for named services is setting up these primitives to begin with, so why have them at all? These (annoyingly) open the possibility of conflating a kernel primitive with a structure that really only exists in userspace, between programs which happen to agree on a communication protocol based on the data structure that does actually exist between them: a single, shared read/writable page, which may or may not be structured in any particular way.
In any case, it appears that actually assigning them a name may be somewhat redundant: assigning them a specific integer for their ID would be equally effective, but since pantheon already asserts all names must be precisely 8 characters and are treated as a big endian integer anyway, this is already essentially how this is done.
Beta Was this translation helpful? Give feedback.
All reactions