cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
The basis is 230k as S-expressions but removing it from the sexpr-bootstrap compiler (unscientifically by editing the sexp file) shrinks the binary by 7197k, so replacing the current basis init...
Right now it seems like we're allocating heap objects and generating very long strings of byte moves: ``` 4fa534: be 2e 00 00 00 mov $0x2e,%esi 4fa539: 40 88 30...
Currently most of what you want is either in old papers or in the code; we should have a document that is continuously updated and cross-referenced so that a complete...
Would be nice to cut the memory usage of the explorer and anything else in half. The basic mark-compact algorithm is not that complicated but the generational collector resulted in...
The only labels that need to be 2-byte aligned are the ones that could potentially be seen by the GC, which is effectively only the ones at the start of...
* x64: This isn't wrong, but it's the Microsoft name for the target in a codebase that otherwise largely assumes Unix? * arm8: There are Armv8 chips that support only...
I have a hunch that for the special case we care about - evaluating monomorphic functions which are extractable to ML on ground arguments - we can do significantly better...
For data whose tag and length can be completely represented in its pointer, there should be no need for a header word. This involves changing the `data_to_wordProps` invariants.
The x64 generated code adds %r14 to every pointer prior to dereferencing it. This seems like a useful feature to have, since it allows a heap anywhere in the address...
`bvi_aux`, `bvl_stub`, and `dec` are only so useful when you have hundreds of each. We should be able to find relevant identifiers in the source and assign _some_ interpretable name...