i feel that the grammar of a programming language is among the least appropriate of all possible facets of its behavior to start off with.
-
Proof creation has a high cost associated with it.
yeah you keep saying it sucks. aren't you supposed to fix things like that
To give an idea, it has been the author’s experience [93, 94, 96] that, in an interactive theorem prover, verifying the functional correctness of C code can require between one and two orders of magnitude more proof steps than line count,
(a) yeah maybe cause you keep trying to verify functional correctness guarantees about heap allocations in ring 0
(b) "line count" appeals to the VC class. it doesn't work on programmersliterally everyone go read aaron turon's paper on weak atomic memory orderings right now https://plv.mpi-sws.org/gps/paper.pdf yes there's a coq proof but that's not what a paper is for!!!
check out this future work section:
However, the C11 model allows programmers to freely mix memory orderings, and ideally program logics should support such mixed reasoning as well.
literally it's that easy to give a shit about making people safe and providing powerful robust guarantees. this is why rust used to be good
Early investigation suggests that the C11 model has some corner cases when mixing memory orderings that may obstruct compositional reasoning principles.
i get nerd sniped every time i read that line lmao
-
literally everyone go read aaron turon's paper on weak atomic memory orderings right now https://plv.mpi-sws.org/gps/paper.pdf yes there's a coq proof but that's not what a paper is for!!!
check out this future work section:
However, the C11 model allows programmers to freely mix memory orderings, and ideally program logics should support such mixed reasoning as well.
literally it's that easy to give a shit about making people safe and providing powerful robust guarantees. this is why rust used to be good
Early investigation suggests that the C11 model has some corner cases when mixing memory orderings that may obstruct compositional reasoning principles.
i get nerd sniped every time i read that line lmao
We believe the extra generality of GPS is important because it enables us to verify a wider class of weak memory programs, including those whose observable behavior is not SC. The circular buffer and Michael-Scott queue are good examples of this (see the appendix [1]). Singh et al. [35] argue that one should not expose the high-level programmer to such non-SC data structures, but GPS shows that in fact it is possible to reason sensibly and modularly about them.
keep in mind seL4 doesn't even represent concurrent behavior at all in their 2009 proof (as far as i can tell), even though concurrency semantics are a feature on any system with a motherboard. and aaron turon shows actually we can make it easier to write complex code with formal verification
-
We believe the extra generality of GPS is important because it enables us to verify a wider class of weak memory programs, including those whose observable behavior is not SC. The circular buffer and Michael-Scott queue are good examples of this (see the appendix [1]). Singh et al. [35] argue that one should not expose the high-level programmer to such non-SC data structures, but GPS shows that in fact it is possible to reason sensibly and modularly about them.
keep in mind seL4 doesn't even represent concurrent behavior at all in their 2009 proof (as far as i can tell), even though concurrency semantics are a feature on any system with a motherboard. and aaron turon shows actually we can make it easier to write complex code with formal verification
honestly i should totally mess around with coq semantics for my ring buffer from hell
-
honestly i should totally mess around with coq semantics for my ring buffer from hell
oh yeah the other guy was telling me how much it sucks to verify stuff
and in a single person year, we may be limited to verifying no more than something in the order of 1000 lines-of-code (LoC). Little data exists for how proof-based projects scale, but it is unlikely to be linear.
still just ridiculous that this guy is still talking "verification" without doing the work in the c compiler. i know people do that
The economics of verification have two significant consequences.
so bleak to talk about your research focus like this
First, the range of systems we can hope to verify is limited, but is still large enough to be practically interesting.
that's literally not a "consequence" why would you invoke proof jargon incorrectly lmao
Modern microkernels, with implementations around 10,000 LoC are hopefully within the realm of possibility.
you were just a moment ago saying
int * p; int * q;was beyond your abilities -
honestly i should totally mess around with coq semantics for my ring buffer from hell
@hipsterelectron "ring buffer from hell" sounds incredibly exciting
-
oh yeah the other guy was telling me how much it sucks to verify stuff
and in a single person year, we may be limited to verifying no more than something in the order of 1000 lines-of-code (LoC). Little data exists for how proof-based projects scale, but it is unlikely to be linear.
still just ridiculous that this guy is still talking "verification" without doing the work in the c compiler. i know people do that
The economics of verification have two significant consequences.
so bleak to talk about your research focus like this
First, the range of systems we can hope to verify is limited, but is still large enough to be practically interesting.
that's literally not a "consequence" why would you invoke proof jargon incorrectly lmao
Modern microkernels, with implementations around 10,000 LoC are hopefully within the realm of possibility.
you were just a moment ago saying
int * p; int * q;was beyond your abilitiesVerification of such systems can bring significant improvements to the reliability of the entire software stack, as above the microkernel layer hardware protection domains limit the impact any incorrectly behaving software has on the trusted computing base [83].
- microkernels don't consider it their problem to provide any sort of correctness guarantees except for their own behavior, so this is just a lie.
- the MMU isolation is from the CPU, not the microkernel
-
Verification of such systems can bring significant improvements to the reliability of the entire software stack, as above the microkernel layer hardware protection domains limit the impact any incorrectly behaving software has on the trusted computing base [83].
- microkernels don't consider it their problem to provide any sort of correctness guarantees except for their own behavior, so this is just a lie.
- the MMU isolation is from the CPU, not the microkernel
i will literally die mad about how casually they mentioned fucking shared memory pages are a replacement for sequenced writes https://trustworthy.systems/publications/nicta_full_text/8988.pdf
In original L4, “long” messages could specify multiple buffers in a single IPC invocation to amortise the hardware mode- and context-switch costs.
a single crumb of structured I/O
While long IPC provides functionality that cannot be emulated
literally the actual criterion for minimality
Shared buffers can avoid any explicit copying be-
tween address spaces"microkernel layer hardware protection domains" cmon
-
i will literally die mad about how casually they mentioned fucking shared memory pages are a replacement for sequenced writes https://trustworthy.systems/publications/nicta_full_text/8988.pdf
In original L4, “long” messages could specify multiple buffers in a single IPC invocation to amortise the hardware mode- and context-switch costs.
a single crumb of structured I/O
While long IPC provides functionality that cannot be emulated
literally the actual criterion for minimality
Shared buffers can avoid any explicit copying be-
tween address spaces"microkernel layer hardware protection domains" cmon
The result was significant kernel complexity, with many tricky corner cases that risked bugs in the implementation.
i thought that's why we used formal verification? that's why microkernels were worth the cost of proofs?
-
The result was significant kernel complexity, with many tricky corner cases that risked bugs in the implementation.
i thought that's why we used formal verification? that's why microkernels were worth the cost of proofs?
after reading all this my impression continues to be that microkernels don't do enough isolation at all!!! i even dug up build systems a la carte https://www.microsoft.com/en-us/research/wp-content/uploads/2018/03/build-systems-final.pdf where simon peyton-jones tried to pull this same shit about build systems
-
after reading all this my impression continues to be that microkernels don't do enough isolation at all!!! i even dug up build systems a la carte https://www.microsoft.com/en-us/research/wp-content/uploads/2018/03/build-systems-final.pdf where simon peyton-jones tried to pull this same shit about build systems
i do actually appreciate that seL4 has a lot of use in single-core embedded applications where you're typically not just greedy for i/o like me and the purpose of an OS actually aligns reasonably well with the atomic i/o APIs
-
after reading all this my impression continues to be that microkernels don't do enough isolation at all!!! i even dug up build systems a la carte https://www.microsoft.com/en-us/research/wp-content/uploads/2018/03/build-systems-final.pdf where simon peyton-jones tried to pull this same shit about build systems
@hipsterelectron one of my gfs and I have a concept that has never been done before which we are working on in fits and starts which I think does what you want, or at least partway. the idea of extreme isolation, no longer having the idea of system calls at all but "cross-calling" and there being a dogmatic principle that ensures authority always and only ever flows from the user. everything can be halted, resumed, disassembled on the fly, etc, but only with direct user authority. I felt like we'd found a grail. It only works in a very small amount of x86-64 code rn kept private to avoid exposure before it is ripe but there's fully a way. not hurd, not a mircokernel, not a monolith, but a sherpa guide
-
i do actually appreciate that seL4 has a lot of use in single-core embedded applications where you're typically not just greedy for i/o like me and the purpose of an OS actually aligns reasonably well with the atomic i/o APIs
For seL4 there are even stronger reasons for staying away from supporting long messages: The formal verification approach explicitly avoided any concurrency in the kernel [Klein et al. 2009], and nested exceptions introduce a degree of concurrency.
i also very specifically want to avoid introducing subtle concurrency bugs but i'm doing that by expanding "isolation" beyond the MMU and expanding named "synchronization contexts" to structure literally all the externally-visible state changes like i/o
i absolutely don't think i could do seL4 better, and i'm not planning to inject tons of confusing and poorly-documented semantics like linux
-
For seL4 there are even stronger reasons for staying away from supporting long messages: The formal verification approach explicitly avoided any concurrency in the kernel [Klein et al. 2009], and nested exceptions introduce a degree of concurrency.
i also very specifically want to avoid introducing subtle concurrency bugs but i'm doing that by expanding "isolation" beyond the MMU and expanding named "synchronization contexts" to structure literally all the externally-visible state changes like i/o
i absolutely don't think i could do seL4 better, and i'm not planning to inject tons of confusing and poorly-documented semantics like linux
at first i was thinking "let's literally just add buffers between everything" but then i got hooked on transactions
-
at first i was thinking "let's literally just add buffers between everything" but then i got hooked on transactions
the one concurrency i will have to figure out is multiple processes writing to the same synchronization domain at once. i think i'm gonna try my damndest to avoid having to use any red-black trees. maybe i'll make it possible to open the same file/shm mapping rw in two+ threads/processes at once but you have to explicitly tell me you actually want me to handle possibly-concurrent write requests to this shared resource
-
the one concurrency i will have to figure out is multiple processes writing to the same synchronization domain at once. i think i'm gonna try my damndest to avoid having to use any red-black trees. maybe i'll make it possible to open the same file/shm mapping rw in two+ threads/processes at once but you have to explicitly tell me you actually want me to handle possibly-concurrent write requests to this shared resource
i also got upset about pipes when i learned even though userspace uses them like ring buffers their semantics just encode the whole monolithic memory architecture i h8. they're literally just a fixed-size queue for atomically pushing/pulling some floating pages
-
i also got upset about pipes when i learned even though userspace uses them like ring buffers their semantics just encode the whole monolithic memory architecture i h8. they're literally just a fixed-size queue for atomically pushing/pulling some floating pages
i have such a negative ranty post i haven't sent from many hours ago but seL4's autobio paper ending with the very clear remark "we can't figure out how to schedule anything, nothing works" -- i didn't see that as like indicative of moral decline. to me it was clarifying!
i also felt this way learning that linux and openbsd also schedule their processes the exact same way seL4 does (to my mind at least), which is generally round-robin
it's actually kinda absurd thinking about how scheduling based upon something besides fair slicing ends up imposing this huge huge huge change in the way the entire system operates!
-
i have such a negative ranty post i haven't sent from many hours ago but seL4's autobio paper ending with the very clear remark "we can't figure out how to schedule anything, nothing works" -- i didn't see that as like indicative of moral decline. to me it was clarifying!
i also felt this way learning that linux and openbsd also schedule their processes the exact same way seL4 does (to my mind at least), which is generally round-robin
it's actually kinda absurd thinking about how scheduling based upon something besides fair slicing ends up imposing this huge huge huge change in the way the entire system operates!
not just me being contrarian when i say driving scheduling from the active data dependency graph is really fascinating to consider too because that's also exactly where it would make sense to update the page attribute table
-
not just me being contrarian when i say driving scheduling from the active data dependency graph is really fascinating to consider too because that's also exactly where it would make sense to update the page attribute table
and telling the CPU to schedule my pages while then scheduling the task that's gonna want them sounds so cute
-
and telling the CPU to schedule my pages while then scheduling the task that's gonna want them sounds so cute
like the only reason i will ever get around to actually doing this is because i want to have extremely deep control over where and how memory flows (including persisted)
and i'm still excited about this bc there's no atomic globally visible changes ever (maybe i/o devices) which is the stuff that makes my brain hurt when linux does it
-
like the only reason i will ever get around to actually doing this is because i want to have extremely deep control over where and how memory flows (including persisted)
and i'm still excited about this bc there's no atomic globally visible changes ever (maybe i/o devices) which is the stuff that makes my brain hurt when linux does it
how simple do my stateful message queues need to get before i can start pretending it's kind of like formal verification
