Promise-First Optimization #32
Conversation
febyeji
force-pushed
the
optimization/tlb
branch
from
715674f to
bb97b5c
Compare
febyeji
force-pushed
the
optimization/promise-first
branch
3 times, most recently
from
15fe070 to
6cb9488
Compare
febyeji
force-pushed
the
optimization/tlb
branch
from
f47a6be to
4e2ef21
Compare
febyeji
force-pushed
the
optimization/promise-first
branch
3 times, most recently
from
462d519 to
9f1f977
Compare
|
Would it be better to move the redundant code for executable models to |
febyeji
force-pushed
the
optimization/tlb
branch
from
4e2ef21 to
dfe8ec8
Compare
febyeji
force-pushed
the
optimization/promise-first
branch
from
9f1f977 to
b898dc2
Compare
febyeji
force-pushed
the
optimization/tlb
branch
from
dfe8ec8 to
4098260
Compare
febyeji
force-pushed
the
optimization/promise-first
branch
3 times, most recently
from
4af0adb to
984fc1b
Compare
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
There are some organisational things to fix, but the main structure is there and correct
febyeji
force-pushed
the
optimization/tlb
branch
from
332e19b to
77afd8b
Compare
febyeji
force-pushed
the
optimization/promise-first
branch
from
984fc1b to
d1798c9
Compare
Fix VM_promising_exe Pass MP, MPDMBS tests with address translation
febyeji
force-pushed
the
optimization/promise-first
branch
3 times, most recently
from
769b651 to
80b7aad
Compare
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
Still some algorithmic clean up, but we're getting there. I didn't make any comments on VMPromsing but anything I said on UMPromising still holds. Also please rebase on main before we can merge.
- Apply code reviews Apply code reviews
febyeji
force-pushed
the
optimization/promise-first
branch
from
533182a to
53d1c39
Compare
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
Sorry if I wasn't clear, my goal was to keep running the old algorithm (CPState.run) in all tests where it's not too slow. I just wanted to reduce the duplication of the per-model functions, which is achieved: Neither UMPromising nor VMPromising has any code that is specific to promise-free or the naive runner. Also some minor style+error message comment.
Although I will wait until after the camera-ready deadline for POPL (2 Dec 26) to merge, sorry
|
|
||
| (* TODO state some soundness lemma between Promising_to_Modelnc and | ||
| Promising_Modelc *) | ||
| <$> CPState.run_promise_first prom term fuel. |
There was a problem hiding this comment.
Promising_to_Modelc should still use run and we should have Promising_to_Modelc_pf as an additional thing, ideally, and tests should run both. Sorry if it wasn't clear
There was a problem hiding this comment.
Oh, sorry. I will fix it.
using
Timetactic