Tracker for PIEO tree compilation

[polybeandip]

@anshumanmohan describes a natural extension of Formal Abstractions' compilation procedure to handle non-work conserving behavior in discussion #16. The hope is that we can simply swap PIFOs in our tree for PIEOs to allow packets to live in our PIEO tree while remaining invisible until they're ready.

See issue #12 for an introduction to @KabirSamsi's work on PIEOs.

This issue is a concrete plan for formalizing PIEO trees and implementing them at the software level.

Extend Formal Abstractions for Packet Scheduling

Each of these tasks map cleanly to parts of Formal Abstractions, which are noted accordingly.

• [x] Describe the semantics and structure of PIEO trees (§3) Write inference rules answering the following questions:
  • [x] What is a PIEO tree?
  • [x] How do you pop a PIEO tree?
  • [x] How do you push to a PIEO tree? What is the data of a path?
  • [x] How do we model scheduling transactions?
• [x] Define simulation for PIEO trees (§4)

• [x] Construct PIEO tree analogues for sections §5.2 to §5.5 in Formal Abstractions

  • [x] Describe how to lifting embeddings.
  • [x] Prove pop is preserved (Lemmas 5.6 and 5.7 Formal Abstractions).
  • [x] Prove push is preserved (Lemmas 5.8 and 5.9 in Formal Abstractions).

  Hopefully, by the end of all this, Theorems 6.1 and 6.2 can be used as is.

Done via #35

Extend pifo-trees-artifact

• [x] Tweak lib/path.ml to accommodate the semantics and structure of PIEO trees (not necessary)
• [x] Make files lib/pieotree.ml and lib/pieotree.mli and implement a PIEO tree in it
• [x] Explore how to alter lib/control.ml and lib/alg.ml to build NWC algorithms via PIEO trees
  • [x] Write a NWC algorithm, make a picture, and debug the algorithm until the picture looks convincing
  • [x] Compile to a different tree shape and make the same picture from that

Done via #1 in schedulers-in-ocaml

[anshumanmohan]

Thanks for getting this down; super helpful! I'm super excited, especially if it just works as elegantly as I am hoping. One quick thing to add after your last bullet point: test compilation "by eye", by generating scheduling graphs in the style of Formal Abstractions. That is:

1. Write a NWC algorithm using one tree shape, make a picture, and debug the algorithm until the picture looks convincing.
2. Compile to a different tree shape and make the same picture from that.

Please just edit your text above directly to include this.

In silly logistical land: feel free to convert certain bullet points into issues of their own and then assign them to yourself. I'll show you how in a sec!

[anshumanmohan]

@polybeandip for the fork under cucapra, try this?

[polybeandip]

For completeness and the benefit of others reading this, here's the fork.