search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

Linear scan register allocation #458

Closed tanyongkiam closed 6 years ago

tanyongkiam commented 6 years ago

This issue (suggested by Magnus) is about writing a linear scan register allocator for CakeML.

This could be very useful when integrated with the CakeML compiler, e.g. when we get a read-eval-print loop, we would want to run a faster allocation algorithm.

This issue can have many scales: a BSc-level project might simply implement an unverified version (replacing the allocator in unverified/reg_alloc), while a MSc-level project could verify the algorithm, and integrate it with the word_alloc's correctness theorem.

tanyongkiam commented 6 years ago

Some additional notes: 1) for integration with wordLang, it might be best to split out the current "conventions" pass in the SSA step and instead do this at the end of wordLang. This is to avoid having large live ranges for certain variables. (this might be avoidable by having smarter live range computation). The new allocator should (preferably) also re-use word_alloc's correctness theorem.

2) see e.g. http://web.cs.ucla.edu/~palsberg/course/cs132/linearscan.pdf for a description of the algorithm

3) Verified Spilling and Translation Validation with Repair, ITP 2017 is also related,

oskarabrahamsson commented 6 years ago

I think this could be useful:

Linear Scan Register Allocation on SSA Form. https://dl.acm.org/citation.cfm?doid=1772954.1772979