PIEO Trees for Fun and Profit #16
Replies: 3 comments 12 replies
-
This does make sense, and it seems quite promising! Like you, I haven't thought through the details of how the compilation would work, but it seems extremely plausible that it would. To summarize, a different way to put this proposal is:
Does that sound like an accurate summary? Anyway, this is all to say it seems quite plausible and seems like a nice, clean generalization! |
Beta Was this translation helpful? Give feedback.
-
I've been thinking about formalizing PIEO trees (issue #19) and more broadly extending the math in the Formal Abstractions (tracker #17) along the lines @anshumanmohan describes above. This branch includes my (flawed) notes on this effort; relevant files: notes.tex and notes.pdf I'd like to take this comment to describe the obstacles I've faced with issue #19. Let's consider the following snapshot of a PIEO tree, with topology Fig 1: snapshot of PIEO tree Just as with PIFO trees, we'd like PIEOs on leaves to contain packets while PIEOs on internal nodes contain pointers to their subtrees. Hence, the
We want to come up with a way to color the
This is the coloring we desire for the root PIEO of Fig 1. Fig 2: snapshot of PIEO tree (with more colors!) The key here is that the color of So far, it seems like we have a sense for the kind of invariant we'd like to enforce, but how do we do it? @anshumanmohan made a suggestion in the top-level post:
While his approach is specific to the Unfortunately, approaches like these, based around decorating pointers in internal PIEOs, don't work well. This is because a pointer to the Fig 3: counter-example to meta-data strategy Fig 3 is the result of pushing packet A few questions:
|
Beta Was this translation helpful? Give feedback.
-
For completeness and the benefit of others reading this, PR #35 (and issue #17) prove the compilation procedure here works! |
Beta Was this translation helpful? Give feedback.
-
Sivaraman et al. claim that PIFO trees can handle non-work conserving behavior, and detail a mechanism that involves, for each node that desires non-work conserving behavior:
I'll let you work through the details in §2.3 of the paper, but the overall point is that a packet that is enqueued may not immediately be ready for
pop
ping. A quick description of their mechanism:push
, the node's shaping transaction is run to determine when the packet will be ready. The packet gets enqueued into the target leaf but not into the ancestor nodes above it, violating Formal Abstractions' condition of well-formedness. The packet also gets enqueued into the shaping PIFO, ranked by the time computed for that packet by the shaping transaction.push
is thus finally complete. Well-formedness is restored.pop
ped as usual.This whole thing is rather janky and was dropped from the formalism in Formal Abstractions. In particular, if you work through this carefully, you will notice that nothing actually shields this special packet from being
pop
ped by some previously enqueued downward reference in the tree! I have an email correspondence with Sivaraman where I confirm this using a little adversarial workflow.My thesis is that:
PIEOs instead of PIFOs
For each node that desires non-work conserving behavior, we should use a PIEO instead of a PIFO. Unrelated parts of the tree can continue to be PIFOs, but see my note below about ancestors of PIEO nodes.
This PIEO should use the predicate
is_ready_at: time -> packet -> bool
, partially applied with the current time. Sois_ready_at time.now
is indeed a predicate on packets. Caution,time.now
is just an opaque thing I've cooked up; we'll need to make it more crisp.Each ancestor of the PIEO node will also need to be a PIEO. These PIEOs store integer indices, and will need to use the predicate
is_ready_at: time -> int -> bool
, again partially applied as sketched above. For simplicity let's say the entire tree's non-work conserving nodes (leaves and internal nodes) use the same policy,is_ready_at: time -> int_or_packet -> bool
.Perk 1 of this approach are that we are always well-formed. Say a packet
p_9
is enqueued at time 0. This packet is going to be ready only after time 9. This packet is fullypush
ed, all the way from the root to the leaf, by computing some path for it as described in Formal Abstractions. Wherever Formal Abstractions' scheduling transaction would have had us enqueue some indexi
into some ancestor node, we'll enqueuei_9
, meaning thati
will only be valid after time 9. No matter when you check well-formedness, this tree is well-formed. At time 0, it is well-formed but some coherent path is not going to answer tois_ready_at 0
. At time 10, the tree is still well-formed and the entire tree also happens to answer tois_ready_at 10
.Perk 2 is the big one: packets that are meant to be invisible until some time actually remain invisible!
Compilation for Free
If we do as I propose, we may just be able to use the tree-to-tree compiler from Formal Abstractions wholesale.
This assertion requires a lot more thinking, but I have gotten excited by the possibility that a tree that is set up per my proposal will happily go through Formal Abstractions' compilation procedure! That is, we can create an topology-to-topology embedding
f
per §6, liftf
tof-hat
§5.2, massage things just a tiny bit more, and watchpush
andpop
be preserved.The lifting is, of course, the tricky part. Basically the existing lifting regime stretches insertion paths as needed to bridge over newly inserted transient nodes. Paths are stretched by dropping irrelevant path entires and duplicating some other path entries along with their ranks. The new lifting regime would similarly extend insertion paths, now duplicating path entries' ranks as well as their earliest dequeue times (
9
in the example above) as needed.Beta Was this translation helpful? Give feedback.
All reactions