FA24 Progress Tracker – Kabir

[KabirSamsi]

This discussion serves to mark my progress throughout the semester, benchmarking a series of tasks I need to work through.

Arbiter Development

Develop and integrate a type system for Rio

• Develop theoretical type system
• Formal definitions for policy sets, set-to-stream and stream-to-stream rules, queues
• Develop the Union operator as a pre-typing safety check on Set-to-Stream policies
• Cross-check system with holistic project plan and formalize typing rules and set partitioning for all policies
• Cross-check with Cassandra's work to update sets and typing rules as is necessary
• Integrate typechecking into Rio's compiler/interpreter for well-formedness
• Store type system and typing rules as artefact in Rio codebase

Develop Operational Semantics for Rio

• Develop theoretical operational semantics
• Cross-check, present work at meeting and translate into formal restrictions for PIFO tree definitions
• Store formal operational semantics as artefact in Rio codebase

Develop QueueGen Arbiter For Rio $\rightarrow$ CalyxQueue Compilation

• Define formally a set of policy-queue structure pipelines
• Develop architecture for arbiter model – i.e. general design for an intermediary flow representation
• Develop OCaml pipeline to generate said IR
• Develop Python arbiter to determine queue structure from IR

[KabirSamsi]

10/1 Log

I've decided that the best step for me before going forward with architecting the arbiter is to lock down clear rules on what kinds of flows we might deal with. As per the discussion with Nate, it seems to me that the best way to do this is to formalize semantics for how flows can simplify down to a compileable state, and a type system to determine exactly which kinds of flows we allow.

Hence, I spent a bit of time on #63, which tackles #62 and presents a first-draft type system for the language, along with a handful of other formalizations which may prove useful. I've designed my own type systems before, but this one has a different air to it – moreso that rather than being a cornerstone of the language, it's more, security guard, less dictator.

At the time of writing this, I don't know if the team has viewed the discussion in full, but I intend to discuss it and more informal thoughts I have on the topic at today's meeting. Once we lock this down, it'll be time to jump to operation Union and perhaps some work on integrating this with the well-formedness interpreter!