You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This issue is about investigating whether the lab_to_target compiler phase can be made faster for in-logic compilation. The current implementation of lab_to_target almost forces computation to be a tedious global process.
Suggestion: one could possibly modify the lab_to_target phase so that a large part of the computation can be done in parallel for each function in the in-logic compilation. One could e.g. compute a maximum encoding length for each function and then assume in other parts that this is the function's exact length. If the encoding turns out to be shorter, then one can add padding at the end to make the function's encoding in order for the actual encoding to always be the maximum encoding length.
Since the lab_to_target phase is complicated and its verification proof is delicate, I suggest trying to make minimal changes before more adventurous changes are attempted.
Note: The lab_to_target compiler must not be changed on master before the install-and-run branch has been merged. Thus any immediate work on this should be a fork off of install-and-run.
The text was updated successfully, but these errors were encountered:
This issue is about investigating whether the
lab_to_target
compiler phase can be made faster for in-logic compilation. The current implementation oflab_to_target
almost forces computation to be a tedious global process.Suggestion: one could possibly modify the
lab_to_target
phase so that a large part of the computation can be done in parallel for each function in the in-logic compilation. One could e.g. compute a maximum encoding length for each function and then assume in other parts that this is the function's exact length. If the encoding turns out to be shorter, then one can add padding at the end to make the function's encoding in order for the actual encoding to always be the maximum encoding length.Since the
lab_to_target
phase is complicated and its verification proof is delicate, I suggest trying to make minimal changes before more adventurous changes are attempted.Note: The
lab_to_target
compiler must not be changed onmaster
before theinstall-and-run
branch has been merged. Thus any immediate work on this should be a fork off ofinstall-and-run
.The text was updated successfully, but these errors were encountered: