Type System For Rio

[KabirSamsi]

Overview

The necessity for a type system in Rio becomes increasingly apparent as we try to strategically restrict what permutations of flow hierarchies are possible. We'll document our progress here. For the time being, we restrict our conversation to only Work-Conserving Algorithms.

As @csziklai's work on understanding which flows motivate hierarchical structure develops, I anticipate the type system will develop as well (it would be lovely if we could design the system such that all that needs to really update as more information comes in is Pol, StreamStream and SetStream (defined below), but it might be a bit early to tell that yet).

However, for the time being, we can simply utilize the set-to-stream and stream-to-stream definitions to our advantage, and define types around that.

---

Contexts

We define a few sets to help us formally describe things later on:

Let $Clss$ represent define a mutable class context. To aid us in formalizing this, we utilize the rule that all classes must be declared at the head of a program. This is outlined as an invariant in #39. In which case, we tidily store all classes in $Clss$, and can use this to formalize that any program with an undefined class is ill-typed.

(Note that a chunk of this hard work is already done in #37, but we log it as a typing rule too).

Let $Pol$ represent our set of policy constructors – i.e.

$$Pol := (RR, Strict, WFQ \dots)$$

Let $SetToStream$ represent the set of set-to-stream policies:

$$SetToStream := (EDF, SJN \dots)$$

Let $StreamToStream$ represent the set of stream-to-stream policies:

$$StreamToStream := (RR, Strict, Fifo \dots)$$

The following should hold:

$$\begin{cases} SetStream \cup StreamStream = Pol\\ SetStream \cap StreamStream = \emptyset \end{cases} $$

That is to say, every policy constructor must be one, and exactly one, of the two types.

---

Simplified Type System

$$\tau := \textbf{set} | \textbf{stream}$$

Typechecking Rules:

$$\frac{c \in \text{Clss}}{c : \textbf{set}}\hspace{0.2cm}\text{T-CLASS}$$

$$\frac{\Gamma \vdash c_1 : \textbf{set} \land \dots c_n : \textbf{set}}{\text{Union}(c_1 \dots c_n) : \textbf{set}}\hspace{0.2cm}\text{T-UNION}$$

$$\frac{\Gamma \vdash c : \textbf{set} \hspace{0.5cm} pol \in SetToStream}{\text{pol}(c) : \textbf{stream}}\hspace{0.2cm}\text{T-SET-STREAM}$$

$$\frac{\Gamma \vdash c_1 : \textbf{stream} \land \dots c_n : \textbf{stream} \hspace{0.5cm} pol \in StreamToStream}{\text{pol}(c_1 \dots c_n) : \textbf{stream}}\hspace{0.2cm}\text{T-STREAM-STREAM}$$

AST modification of Weighted-Fair-Queueing:

| WeightedFair of stream list * float list

Gives the final typing rule:

$$\frac{\Gamma \vdash c_1 : \textbf{stream} \land \dots c_n : \textbf{stream} \hspace{0.5cm} \hspace{0.5cm} d_1 \in \mathbb{R} \land \dots \land d_n \in \mathbb{R}}{WFQ(\{c_1 \dots c_n\}, \{d_1 \dots d_n\}) : \textbf{stream}}\hspace{0.2cm}\text{T-WFQ}$$

[KabirSamsi]

(Please bear with me as my formatting is torn to bits in GitHub's latex editor ... I will get better with time).

To which effect, I think once this is crisped up and reviewed a bit, should be kept as an document somewhere in the codebase itself rather than as a discussion. I want this to be a point of departure, though, so I'm holding off on that for now.

[KabirSamsi]

I'm worried about wclss, upon going through my work again. It's an outlier, and corresponds how the clss * int type for WFQ sticks out in the AST. Any thoughts for how to deal with this?

[KabirSamsi]

A thought I had was that we could enforce that all policies can take in either classes or weighted classes; unless specified, they should ignore the second argument of wclass tuples.

[anshumanmohan]

Cool stuff!

I'm excited for you to say more at the meeting, but just a few notes in the meantime:

• I get the English explanation of $$\in_{set \rightarrow stream}$$ but am getting lost in the notation.
• I'm also getting lost in the notation of foo -> bar vs FooBar.
• Sorry to nitpick, but are $$clss$$ and $$Clss$$ meant to be different? What about $$setstream$$ vs $$SetStream$$, $$streamstream$$ vs $$StreamStream$$?
• Re: the actual rules, my stance is that:
  • Sets can be unioned together to make a set.
  • Sets can be converted into a stream using a Set2Stream policy.
  • Streams can be orchestrated into a single stream using a Stream2Stream policy.
  • This sorta answers your two questions towards the bottom of your note: no, and no. But anyway let's talk more IRL and firm up what we think as a team.
• I agree that wclss is a bit of a sore thumb but that's okay with me!

[polybeandip]

Do we actually need a type system for our set and stream setup? Could we not instead tweak Rio's grammar?

For example, does this AST do the trick?

type clss = string
type var  = string

type set = 
  | Class of clss
  | Union of set list

type stream = 
  (* set2stream *)
  | Fifo             of set
  | EarliestDeadline of set
  | ShortestJobNext  of set
  (* streams2stream *)
  | RoundRobin       of stream list
  | Strict           of stream list
  | WeightedFair     of (stream * float) list
  (* variables *)
  | Var              of var

(* not sure how to classify these:
  | ShortestRemaining 
  | RateControlled 
  | LeakyBucket
  | TokenBucket
  | StopAndGo *)

type declare    = clss list
type assignment = var * stream
type return     = stream
type program    = declare * assignment list * return

[KabirSamsi]

It's compelling! Perhaps the type system exists only as a theoretical construct then ... we should probably discuss this.

[KabirSamsi]

(Moving the former updated type system now into the initial discussion).

Per our last two meetings, we've run two new drafts of a type system and come up with one which is:
a) Compact, satisfactorily restrictive & expressive
b) Concretely representable at parser-AST level via @polybeandip's proposed modification to the Operational Semantics.

As we discover new policies, we can verify that each of them correctly typecheck per the above rules.

This should conclude a wrap on the type system for now!