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.
-
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
-
how simple do my stateful message queues need to get before i can start pretending it's kind of like formal verification
this other citation "why do people still use c for high-reliability environments" https://dl.acm.org/doi/10.1145/1215995.1216004 because nowhere else is willing to maintain a lingua franca out of the goodness of their heart
-
this other citation "why do people still use c for high-reliability environments" https://dl.acm.org/doi/10.1145/1215995.1216004 because nowhere else is willing to maintain a lingua franca out of the goodness of their heart
i was thinking about this too after i learned about the caveats with side effect sequencing. i don't think there's anything terribly special about C other than i know gcc devs are genuinely sweet and thoughtful and passionate
-
this other citation "why do people still use c for high-reliability environments" https://dl.acm.org/doi/10.1145/1215995.1216004 because nowhere else is willing to maintain a lingua franca out of the goodness of their heart
@hipsterelectron Bingo. Everyone trying to replace it wants something in return and offers up something largely or entirely unsuitable for systems programming.
-
i was thinking about this too after i learned about the caveats with side effect sequencing. i don't think there's anything terribly special about C other than i know gcc devs are genuinely sweet and thoughtful and passionate
if i wanted to make a language for the macrokernel i would have to decide to understand a lot more than i do now about what the hell a kernel is and especially boot logic. and then i'd have to learn about disk persistence.
i think as an implementation language for managing memory and cpu structures there definitely could be better frontends. and i think once i feel more comfortable about the hardware semantics (particularly x86 cpu + ssd nvme) then i will want to start gernerating structures that translate the macrokernel user API in my head to match the requirements from the hardware
-
if i wanted to make a language for the macrokernel i would have to decide to understand a lot more than i do now about what the hell a kernel is and especially boot logic. and then i'd have to learn about disk persistence.
i think as an implementation language for managing memory and cpu structures there definitely could be better frontends. and i think once i feel more comfortable about the hardware semantics (particularly x86 cpu + ssd nvme) then i will want to start gernerating structures that translate the macrokernel user API in my head to match the requirements from the hardware
like an interlocking web of formal models dancing together in the memory page prairie is actually what i see in my head when i think of the end goal
-
like an interlocking web of formal models dancing together in the memory page prairie is actually what i see in my head when i think of the end goal
look up this paper on "model checking c source code for embedded systems" https://link.springer.com/article/10.1007/s10009-009-0106-5
- buy it for $40! thanks!
two just horrifying suggestions to purchase below that:
- A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning
- Finding software vulnerabilities in large C projects via bounded model checking
-
look up this paper on "model checking c source code for embedded systems" https://link.springer.com/article/10.1007/s10009-009-0106-5
- buy it for $40! thanks!
two just horrifying suggestions to purchase below that:
- A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning
- Finding software vulnerabilities in large C projects via bounded model checking
never sure how to take lines like these https://sci-hub.st/10.1007/s10009-009-0106-5
The disadvantage is that all specific knowledge of the C code and the underlying hardware has to be used in the abstraction process as the general purpose model checkers are not aware of these peculiarities.
i assumed everyone doing this sort of thing was the author of the C code they're checking and that everything of course has to be specialized to the particular CPU. i don't know what anyone would expect to get out of model checking otherwise
-
never sure how to take lines like these https://sci-hub.st/10.1007/s10009-009-0106-5
The disadvantage is that all specific knowledge of the C code and the underlying hardware has to be used in the abstraction process as the general purpose model checkers are not aware of these peculiarities.
i assumed everyone doing this sort of thing was the author of the C code they're checking and that everything of course has to be specialized to the particular CPU. i don't know what anyone would expect to get out of model checking otherwise
actually delighted to hear not only that gcc tends to be the de facto here but that CIL is compatible. CIL sounds sick
If the GCC compiler supports the chosen microcontroller, the adjustments are less costly since many of the C code model checkers use the GCC compiler or a compatible framework such as CIL for preprocessing.
-
this is also pretty worrying because he dismissed earlier ever conforming with the C standard, and seL4 literally just asserts that its C code conforms to the model
@hipsterelectron@circumstances.run i haven't read your whole thread yet, but the important thing about how seL4 does things is that they give a operational semantics for the machine they're targeting too and prove their code in subset-of-C and the resulting binary implement the same thing.
this means that it does not matter whether they conform to the C standard, just that they are a close enough match to the compiler semantics.
the question to worry about is: how correct is their model of the operational semantics of the underlying machines?
-
@hipsterelectron Bingo. Everyone trying to replace it wants something in return and offers up something largely or entirely unsuitable for systems programming.
@dalias @hipsterelectron Also, C never tried to abstract or hide the HW or OS from the programmer. You could and can write a PORTABLE program that constructs and de-references "(char *) null+451", or hooks the system exception handler (at user priv), even does some syscalls.
Nobody tried adding OpenClaw to strcpy() [which is not part of "C" anyway]
-
actually delighted to hear not only that gcc tends to be the de facto here but that CIL is compatible. CIL sounds sick
If the GCC compiler supports the chosen microcontroller, the adjustments are less costly since many of the C code model checkers use the GCC compiler or a compatible framework such as CIL for preprocessing.
yet another seemingly-legit ARPANET paper that seems like it was made to be found discarded in an abandoned laboratory https://people.mpi-sws.org/~gummadi/teaching/sp07/sys_seminar/arpanet.pdf
Attempts at computer networks have been made in the past
"but they weren't evil enough for our purposes".
dude is absolutely crashing out about "load sharing", claiming it will never be worth the cost, and computer programs are incompatible, etc. given that i know that worked for parallel scala compiles, it seemed confusing until the next section
-
yet another seemingly-legit ARPANET paper that seems like it was made to be found discarded in an abandoned laboratory https://people.mpi-sws.org/~gummadi/teaching/sp07/sys_seminar/arpanet.pdf
Attempts at computer networks have been made in the past
"but they weren't evil enough for our purposes".
dude is absolutely crashing out about "load sharing", claiming it will never be worth the cost, and computer programs are incompatible, etc. given that i know that worked for parallel scala compiles, it seemed confusing until the next section
Data Sharing:
The program is sent to a remote computer where a large data bank exists.
This type of operation will be particularly useful where data files are too large to be duplicated economically.so our boy lawrence g. roberts totally predicted bazel cloud builds and github actions.
Access to this data base will be required simply to make an inquiry or may involve executing a complex program using the data base.
mysterious access control mechanisms? potential surveillance? it gets better:
This type of use is particularly important to the military for command and control, information, retrieval, logistics and war gaming applications.
In these cases, one command would send a program to be executed at another center where the data base existed.i really never know if they're just saying intentionally ridiculous shit
note how he distinguishes "send a program" -- clearly an RPC call, which were definitely around at the time
-
Data Sharing:
The program is sent to a remote computer where a large data bank exists.
This type of operation will be particularly useful where data files are too large to be duplicated economically.so our boy lawrence g. roberts totally predicted bazel cloud builds and github actions.
Access to this data base will be required simply to make an inquiry or may involve executing a complex program using the data base.
mysterious access control mechanisms? potential surveillance? it gets better:
This type of use is particularly important to the military for command and control, information, retrieval, logistics and war gaming applications.
In these cases, one command would send a program to be executed at another center where the data base existed.i really never know if they're just saying intentionally ridiculous shit
note how he distinguishes "send a program" -- clearly an RPC call, which were definitely around at the time
fidonet did a ton of load sharing on a per-file basis, including some really interesting locality-based queueing
-
fidonet did a ton of load sharing on a per-file basis, including some really interesting locality-based queueing
Program Sharing: Data is sent to a program located at a remote computer and the answer is returned. Software of particular efficiency or capability exists on certain machines.
literally this is all google tech lmao it's like he's salivating over this
The use of specialized programs at remote facilities makes possible large gains in performance.
Perhaps even more important is the potential saving in reprogramming effort.ridiculous shit
-
This style of definition was used in the definition of Standard ML by Milner, Tofte and Harper [MTH90]. This example, one of the most famous formal language definitions, is a clear demonstration that a large language can be formalised in this manner.
i'm getting the impression that the seL4 HOL C semantics may not be as useful as it's being let on lmao
@hipsterelectron oh wait that's what you're looking at rn??
-
Program Sharing: Data is sent to a program located at a remote computer and the answer is returned. Software of particular efficiency or capability exists on certain machines.
literally this is all google tech lmao it's like he's salivating over this
The use of specialized programs at remote facilities makes possible large gains in performance.
Perhaps even more important is the potential saving in reprogramming effort.ridiculous shit
yeah and then he mentions three separate times how scientists can use it to do new science together. it seems important that scientists are on it at all
