Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Tracker for PIEO tree compilation #17

Open
15 tasks done
polybeandip opened this issue Jun 29, 2024 · 3 comments · May be fixed by #35
Open
15 tasks done

Tracker for PIEO tree compilation #17

polybeandip opened this issue Jun 29, 2024 · 3 comments · May be fixed by #35
Assignees
@polybeandip

Comments

@polybeandip
Copy link
Contributor

polybeandip commented Jun 29, 2024 •
edited
Loading

@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.

  • Describe the semantics and structure of PIEO trees (§3)
    Write inference rules answering the following questions:
    • What is a PIEO tree?
    • How do you pop a PIEO tree?
    • How do you push to a PIEO tree? What is the data of a path?
    • How do we model scheduling transactions?
  • Define simulation for PIEO trees (§4)
  • Construct PIEO tree analogues for sections §5.2 to §5.5 in Formal Abstractions
    • Describe how to lifting embeddings.
    • Prove pop is preserved (Lemmas 5.6 and 5.7 Formal Abstractions).
    • 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

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

Done via #1 in schedulers-in-ocaml
@anshumanmohan
Copy link
Contributor

anshumanmohan commented Jul 1, 2024 •
edited
Loading

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
Copy link
Contributor

@polybeandip for the fork under cucapra, try this?

@polybeandip
Copy link
Contributor Author

polybeandip commented Jul 15, 2024 •
edited
Loading

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

@polybeandip polybeandip linked a pull request Jul 22, 2024 that will close this issue
Open
@anshumanmohan anshumanmohan mentioned this issue Jul 23, 2024
Open
@polybeandip polybeandip self-assigned this Jul 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@polybeandip polybeandip

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Formalize PIEO Tree Compilation cucapra/packet-scheduling
2 participants
@anshumanmohan @polybeandip