Layering

6 Layering

PLAN provides an interesting method of implementing traditional protocol encapsulation.

6.1 Chunks

Essentially, a PLAN computation be made first class by turning it into a chunk (as described in Section 3.1). A PLAN value of type a chunk is specified by surrounding a function's name with |'s at the call site (the a part is determined by the return type of the given function). This newly created chunk can in turn be given as an argument to another function, which itself can be made into a chunk. This function should perform some processing of its own, and then as its last action evaluates the original chunk. This process mimics encapsulation. When the lastly created chunk is sent to the destination and evaluated, each encapsulated chunk is evaluated, the reverse order in which they were made. This process mimics demultiplexing. Examples of how layering is used may be found in Sections 7.2.9 and 7.2.8.

When a chunk is created, a static analysis is performed to determine how much of the code of the invoking packet should be bundled into the newly created chunk. This analysis is conservative in that it will include at least the needed code, and perhaps more. For example, consider the following PLAN program, which implements ping:

svc thisHostIs : host -> bool
svc getRB : void -> int
svc defaultRoute : host -> host * dev

fun ping (source, destination) =
  if (thisHostIs (destination)) then
    OnRemote (|ack| (), source, getRB (), defaultRoute)
  else
    OnRemote (|ping| (source, destination), 
              destination, getRB (), defaultRoute)

svc print : 'a -> unit

fun ack() = print ("Success")

When this packet is sent to ping a remote destination, the ping function will be specified in the initial invocation, therefore at least the code for ping is required. The analysis then looks through the definition of ping for any other chunk creations. It then finds the first one, ack. Because the code for ack may be needed later, when ping is actually invoked, the definition for ack is retained as well.

Here is the conservative part. As the analysis recursively searches the program through its chunk creations, it keeps track of the lowest function definition, and retains all code from the start of the definitions up to that point. This is why the analysis does not have to look at normal function invocations: normal static scoping, which enforces a ``define before use'' model, will take care of correctness there.

Any unneeded code will be pruned. Because of the conservatism of the algorithm, the order of the definitions in the code matters. For example, consider the creation of the ack chunk above at the destination. Because ack is the second function defintion, the code for the ping function will also be retained, even though it isn't needed (ack will never call ping). However, if we reorder the defintions so that ack comes first, the ping code will be properly discarded. A better flow analysis could be less conservative.