[HN Gopher] Cranelift, Part 3: Correctness in Register Allocation ___________________________________________________________________ Cranelift, Part 3: Correctness in Register Allocation Author : lukastyrychtr Score : 20 points Date : 2021-03-19 21:24 UTC (1 hours ago) (HTM) web link (cfallin.org) (TXT) w3m dump (cfallin.org) | monocasa wrote: | Tangentially, one of the most clever things about ebpf IMO is | that it pushes register allocation out to user space and just | verifies that register allocation (or more correctly the full | data flow including the usage of the registers) doesn't break the | VM guarantees. Then the JIT just has a fixed translation of ebpf | registers to machine registers. | | Even compcert (the formally proven compiler with gcc -O2 | competitive code generation) essentially shells out to non proven | ML and then verifies the result in contrast to the rest of the | compiler design. ___________________________________________________________________ (page generated 2021-03-19 23:00 UTC)