Skip to content

Linearization

gziat requested to merge linearization into main

This MR implements linearization by removing ESEQs and promoting CALLs to the top level. The commutativity check introduced here is more precise than Appel's method, as it analyzes every statement and expression to (over)estimate the set of memory regions they handle. Two statements commute if their associated regions do not intersect or if the intersection only involves read operations.

Merge request reports