Summer Progress Tracker – Anshuman

[anshumanmohan]

Week of July 8

I spent half the week on vacation and brought back something respiratory with me, so this has been a short week.

I returned to a very interesting question from the group about PIEO trees and the invariants they need to maintain. I made the case that the simple solution, while a bit chaotic-feeling, actually does what one would want. Further, it does it with quite some elegance! I think the group mostly agrees with my explanation, but it's certainly worth proving to ourselves very carefully and perhaps even including such a proof in a future publication.

I also reviewed calyxir/calyx#2192: oracles for PIEOs and PCQs, plus a general-purpose and simple-as-possible oracle for NWC policies.

I experimented some with #25: an AST and parser for our DSL. See stack below for a follow-up task.

My stack (ordered vaguely by most overdue to least overdue 😅)

• The lit review actually still has a few TODOs!
• I'd like to expand the glossary to include NWC algorithms so that we can test the Calyx implementations and the OCaml compiler with realistic examples.
• We'd like to extend the DSL to be able to reason about transient nodes, so that the DSL can represent pre- and post-compilation policies. Here "compilation" is used in the Formal Abstractions sense.
• @polybeandip has a couple questions for me in the Slack that I need to get to. This may again involve getting Tobias's advice.
• I was discussing with @csziklai that the AST she showed me on Thursday over Zoom (which was slightly different from the one you can see in Ast, Parser, and Lexer for DSL (v2) #25) may not be quite right. The way she defines a policy (and everything "below" that) looked good to me, but I was a little worried about how she was creating the top-level program. I promised her I would give it a think.
• @polybeandip has a question for me re: the Formal Abstractions codebase. We have a set of PCAPs whose names contain "generated", and I promised him I'd figure out what the story was.

[anshumanmohan]

Week of July 15

Sadly I remained a little sick last week, but I think I'm finally on the mend for real.

I was able to pop off the following from my stack:

• Akash's questions: resolved in Slack
• My thoughts about simplifying Cassandra's ASTs further: came together in DSL: Simplify AST #29
• Akash's questions re: "generated" PCAPS: still a little bit of a mystery tbh, but we have agreed to move on. The important thing that he needed (the ability to packet lengths when making synthetic PCAPs) has been figured out.

My stack (I guess we're following the garbage collection thing of old values living longer...)

• The lit review actually still has a few TODOs!
• I'd like to expand the glossary to include NWC algorithms so that we can test the Calyx implementations and the OCaml compiler with realistic examples.
• We'd like to extend the DSL to be able to reason about transient nodes, so that the DSL can represent pre- and post-compilation policies. Here "compilation" is used in the Formal Abstractions sense.
• @polybeandip has a proof sketch that I'd like to help on.
• Rachit suggested a quick change to generate better parser errors; I'd like to help @csziklai with this if she'd like!

[anshumanmohan]

Week of July 22

I was able to pop the following off my previous stack:

• Expand the Glossary of Scheduling Policies #13 to include NWC algorithms. Done via delegation to @KabirSamsi. Thank you!
• Rachit's suggestion for better parser errors. Fleshed it out, then also passed it on to @KabirSamsi. Thank you!

Minor, but I opened #29 and #42, both of which have been merged. I also reviewed a buncha PRs, which have also been fixed up per my request and merged; I won't go listing them here because they are really the undergrads' achievements and they may want to list them in their notebooks :)

I've also been staging issues all over the place, and the undergrads have snapped up a good few of them! One largish thing is now our queues "flag day", documented in the ever-growing issue calyxir/calyx#2191. It would be super to get this done before the summer ends and our collective bandwidth gets cut down. We have a ton of info in our heads right now and I think doing flag day (and doing it well) will free us from keeping all that in our heads.

A very fun thing I did was writing up #38. I am excited for this (or something like it) to help stitch together all the work we have thus far.

My new stack, in the order I really ought to complete it:

• @polybeandip has a proof sketch that I'd like to help on. Sorry that I've taken a while with this!
• 🆕 Look over Well-formedness and its preservation in a PIEO tree context #36.
• We'd like to extend the DSL to be able to reason about transient nodes, so that the DSL can represent pre- and post-compilation policies. Here "compilation" is used in the Formal Abstractions sense. Compiler paths: policy DSL to Calyx eDSL #38 has given us additional context about the need for this.
• 🆕 Compiler paths: policy DSL to Calyx eDSL #38 has also inspired me to think a little about the challenging with rewarding "red path", where you compile policy DSL programs to the Caylx eDSL pretty naively, but then need to do a tree-to-tree compilation at the eDSL level. I kinda want to think about this hard tree-to-tree compilation a little and see if I can't just figure it out. This is the kind of thing that can occupy you for weeks and go nowhere, so I promise I will spend ~8 concerted hours on it and then report.
• The Lit Review: Programmable Packet Scheduling on SmartNICs #11 actually still has a few TODOs!

[anshumanmohan]

Week of July 29

Gone fishin' 🎣 🇲🇽

[anshumanmohan]

But I will add that I agreed to team up with @KabirSamsi on his Calyx implementations of PIEOs. In particular we are getting a tad worried that we may be missing something from the OG authors' handwritten Verilog that helps them achieve the speeds that they claim.