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.
-
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
-
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
and i found all that about DARPA salivating over people never writing their own programs again because of:
- the seL4 paper which got best paper https://web.archive.org/web/20110219113850/http://www.ok-labs.com/releases/release/open-kernel-labs-paper-on-formal-verification-wins-top-prize-at-prestigious
still think this paper is terrible. it keeps saying it made compromises for verifiability and wildly overstates the guarantees
turns out that conference SOSP is literally the (ACM) conference whose first year was when a big ARPANET thing was unveiled https://en.wikipedia.org/wiki/Symposium_on_Operating_Systems_Principles
there's these unstructured notes from the fucking pentagon lmao https://web.archive.org/web/20150405055923/https://web.stanford.edu/dept/SUL/library/extra4/sloan/mousesite/EngelbartPapers/B1_F20_CompuMtg.html
and finally this is IETF at its best https://en.wikipedia.org/wiki/Shared_resource choose the most generic possible term that sounds like page cache, but it specifically means network share
-
and i found all that about DARPA salivating over people never writing their own programs again because of:
- the seL4 paper which got best paper https://web.archive.org/web/20110219113850/http://www.ok-labs.com/releases/release/open-kernel-labs-paper-on-formal-verification-wins-top-prize-at-prestigious
still think this paper is terrible. it keeps saying it made compromises for verifiability and wildly overstates the guarantees
turns out that conference SOSP is literally the (ACM) conference whose first year was when a big ARPANET thing was unveiled https://en.wikipedia.org/wiki/Symposium_on_Operating_Systems_Principles
there's these unstructured notes from the fucking pentagon lmao https://web.archive.org/web/20150405055923/https://web.stanford.edu/dept/SUL/library/extra4/sloan/mousesite/EngelbartPapers/B1_F20_CompuMtg.html
and finally this is IETF at its best https://en.wikipedia.org/wiki/Shared_resource choose the most generic possible term that sounds like page cache, but it specifically means network share
oh this is a great tidbit
Before 2023, SOSP was held every other year, alternating with the conference on Operating Systems Design and Implementation (OSDI);
- starting 2024, SOSP began to be held every year.
lots of weird things like this
-
oh this is a great tidbit
Before 2023, SOSP was held every other year, alternating with the conference on Operating Systems Design and Implementation (OSDI);
- starting 2024, SOSP began to be held every year.
lots of weird things like this
oh then i found this guy who was at the arpanet conference http://royalsocietypublishing.org/rsbm/article-pdf/doi/10.1098/rsbm.2002.0006/911101/rsbm.2002.0006.pdf
so like this guy is easily off the charts evil imho. this is him saying he was smarter and braver than alan turing:
My few contacts with Turing were not encouraging. I wanted to talk to him about the remarkable results of his paper ‘On computable numbers’. Reading this paper I had found numerous errors in the formal specification of the universal computer. Some were trivial but others were quite subtle and I was not sure that my solutions were correct. When I came to this point, Turing became more and more agitated, until I could see that no sensible discussion was possible. Clearly he felt the errors to be irrelevant and my drawing attention to them rather foolish.
then he mysteriously advises on "cryptography" from the late 80s until he finally fucked off this planet
Retirement did not by any means imply inactivity. For the next 15 years Davies practised
as a consultant in security engineering for the financial and media industries. This was at a
time when systems based on cryptographic and similar techniques were coming into wide use
both for cash cards and pay television. -
oh then i found this guy who was at the arpanet conference http://royalsocietypublishing.org/rsbm/article-pdf/doi/10.1098/rsbm.2002.0006/911101/rsbm.2002.0006.pdf
so like this guy is easily off the charts evil imho. this is him saying he was smarter and braver than alan turing:
My few contacts with Turing were not encouraging. I wanted to talk to him about the remarkable results of his paper ‘On computable numbers’. Reading this paper I had found numerous errors in the formal specification of the universal computer. Some were trivial but others were quite subtle and I was not sure that my solutions were correct. When I came to this point, Turing became more and more agitated, until I could see that no sensible discussion was possible. Clearly he felt the errors to be irrelevant and my drawing attention to them rather foolish.
then he mysteriously advises on "cryptography" from the late 80s until he finally fucked off this planet
Retirement did not by any means imply inactivity. For the next 15 years Davies practised
as a consultant in security engineering for the financial and media industries. This was at a
time when systems based on cryptographic and similar techniques were coming into wide use
both for cash cards and pay television.omg
Davies was very much an engineer rather than a scientist, and he was always on the lookout
for topics in which his ingenuity and insight could be deployed.guy who steals people's ideas
-
omg
Davies was very much an engineer rather than a scientist, and he was always on the lookout
for topics in which his ingenuity and insight could be deployed.guy who steals people's ideas
He was early in the field of civil uses of cryptography and always had a healthy scepticism of claims to perfection.
terrifying
Mathematical proof of the security of a system struck him as dubious, because it is much easier to prove resistance to attacks one has thought about than it is to prove resistance to attacks one has not thought about.
guy who knows how cryptography works
-
He was early in the field of civil uses of cryptography and always had a healthy scepticism of claims to perfection.
terrifying
Mathematical proof of the security of a system struck him as dubious, because it is much easier to prove resistance to attacks one has thought about than it is to prove resistance to attacks one has not thought about.
guy who knows how cryptography works
omg the EROS author is literally validating all my ideas about the macrokernel love that for me
-
omg the EROS author is literally validating all my ideas about the macrokernel love that for me
Systems programs are strongly driven by bulk I/O
performance.he keeps talking about multiple aliasing being problematic and of course this is why i decided to never share anything and instead have layered i/o queues
In systems code, the effect of representation and data placement can be extreme. Bonwick et al. discuss some of these effects [5], noting that the performance of system-level benchmarks can change by 50% through careful management of cache residency and collisions.
but how do you manage something "carefully" if all the interfaces allow for is urgency???
This tends to penalize the performance of automatic storage reclamation strategies. To make matters more interesting, there are caches.
yeah it rly annoys me how the filesystem has its own caches and the kernel has its own caches but there's this assumption that persistence is always the final destiny of all writes
It follows that user-managed storage is a requirement, but perhaps not in fully general form.
that's exactly it!
-
Systems programs are strongly driven by bulk I/O
performance.he keeps talking about multiple aliasing being problematic and of course this is why i decided to never share anything and instead have layered i/o queues
In systems code, the effect of representation and data placement can be extreme. Bonwick et al. discuss some of these effects [5], noting that the performance of system-level benchmarks can change by 50% through careful management of cache residency and collisions.
but how do you manage something "carefully" if all the interfaces allow for is urgency???
This tends to penalize the performance of automatic storage reclamation strategies. To make matters more interesting, there are caches.
yeah it rly annoys me how the filesystem has its own caches and the kernel has its own caches but there's this assumption that persistence is always the final destiny of all writes
It follows that user-managed storage is a requirement, but perhaps not in fully general form.
that's exactly it!
The facts say otherwise. The annual cost to operate a large banking data center today is $150,000 per square foot. It is by far the most expensive real estate in the world, and more than one third of that cost is the cost of cooling the data center.
2006!!!!
-
The facts say otherwise. The annual cost to operate a large banking data center today is $150,000 per square foot. It is by far the most expensive real estate in the world, and more than one third of that cost is the cost of cooling the data center.
2006!!!!
wait shit he had a point:
The general rule of thumb is that power
is proportional to V2F: the square of the voltage times the frequency. Most of this power is wasted as heat. To a system’s programmer, the cost of doubling the clock rate is $50,000 per square foot per machine room.do i detect an IETF hater???
Raising the clock rate decidedly isn’t free, and walking into the network distribution closet at your business or school will quickly convince you that current power usage is excessive.
