matu3ba

9 ms·

91.
by matu3ba 5y ago
Take a look at my comparison of semantics that unfortunately not yet includes a sketch of memory and synchronization: https://gist.github.com/matu3ba/dda72ad5ee473e3ea26426c121e0...
92.
by matu3ba 5y ago
You need to provide low-level build functions, which is quite some work. On top of that you need to understand the build system of the libcs to replicate it. On top of that for libcs you want to deduplicate all symbols to reduce as much spa
93.
by matu3ba 5y ago
yet.
94.
by matu3ba 5y ago
1. Do you have a blog post with exact instructions for this for some of the platforms? 2. Does this include targeting any gnu libc version (backwards compatible)? This would be very surprising to me.
95.
by matu3ba 5y ago
Please be specific with version numbers. Did you file an upstream bug already? Do you mean https://github.com/BZFlag-Dev/bzflag ? Thats c++ and must be compiled with zig c++.
96.
by matu3ba 6y ago
What tool/framework do they use for annotation and are there standards like SMTlib2, but for annotating those kind of things? Can this tools verify that the annotations are correct wrt the code below or above?
97.
by matu3ba 6y ago
You might be interested in cakeml and cogent. What Safety Integrity Level can ivory guarantee? level2?
98.
by matu3ba 6y ago
Checked as well. They can only do this, because they require that heap memory owned by pointers does not get fragmented. So programmers must manage pointer offsets to each heap structure themself. Hence you never get potential pointer soup
99.
by matu3ba 6y ago
Are there any compiletime benchmarks? I would be interested how much their approach scales in terms of code size, since they use likely SMT solvers to guarantee having no arithmetic overflows (which is more than Rust guarantees). Ideally as
100.
by matu3ba 6y ago
Jakub Konka wrote the M1 linker without any spec in the last half year while having a dayjob at Microsoft.