[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)