On Mon, Jan 30, 2023 at 08:24:00PM +0200, Eduard Zingerman wrote: > + > + +--------------------------+--------------------------+ > + | Frame #0 | Frame #1 | > + Checkpoint +--------------------------+--------------------------+ > + #0 | r0-r5 | r6-r9 | fp-8 ... | > + +--------------------------+ > + ^ ^ ^ > + | | | > + Checkpoint +--------------------------+ > + #1 | r0-r5 | r6-r9 | fp-8 ... | > + +--------------------------+ > + ^ ^ nil nil nil > + | | | | | > + Checkpoint +--------------------------+--------------------------+ > + #2 | r0-r5 | r6-r9 | fp-8 ... | r0-r5 | r6-r9 | fp-8 ... | > + +--------------------------+--------------------------+ Looks like you already realized that frame1 r1-r5 needs to be connected to frame0 r1-r5. Otherwise when subprog (frame1) reads r1 the read mark won't be propagated into checkpoint#1 r1 frame0 and r1 in frame0 will be trimmed incorrectly. > + ^ ^ ^ ^ ^ > + | | | | | > + Checkpoint +--------------------------+--------------------------+ > + #3 | r0-r5 | r6-r9 | fp-8 ... | r0-r5 | r6-r9 | fp-8 ... | > + +--------------------------+--------------------------+ > + ^ ^ > + | | > + Current +--------------------------+ > + state | r0-r5 | r6-r9 | fp-8 ... | > + +--------------------------+ > + \ > + r6 read mark is propagated via > + these links all the way up to > + checkpoint #1. > + ... > +Read marks propagation for cache hits > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > + > +Another important point is handling of read marks when a previously verified > +state is found in the states cache. All read marks present on registers and > +stack slots of the cached state must be propagated over the parentage chain of > +the current state. Function ``propagate_liveness()`` handles this case. > + > +For example, consider the following state parentage chain (S is a > +starting state, A-E are derived states, -> arrows show which state is > +derived from which):: > + > + r1 read > + <------------- A[r1] == 0 > + +---+ C[r1] == 0 > + S ---> A ---> | B | ---> exit E[r1] == 1 > + | | | > + ` ---> C ---> | D | > + | +---+ > + ` ---> E The box around B and D is confusing. The description doesn't explain what the box is for. If the box is removed the description stays as-is, no? > + ^ > + ^ |___ suppose all these > + | states are at insn #Y > + suppose all these > + states are at insn #X > + > +* Chain of states ``S -> A -> B -> exit`` is verified first. > + > +* While ``B -> exit`` is verified, register ``r1`` is read and this read mark is > + propagated up to state ``A``. > + > +* When chain of states ``C -> D`` is verified the state ``D`` turns out to be > + equivalent to state ``B``. > + > +* The read mark for ``r1`` has to be propagated to state ``C``, otherwise state > + ``C`` might get mistakenly marked as equivalent to state ``E`` even though > + values for register ``r1`` differ between ``C`` and ``E``. Overall it's awesome. Please cc Edward Cree <ecree.xilinx@xxxxxxxxx> in the respin.
