--- Date: Wed, 10 Oct 2001 22:03:48 -0700 --- From: Mark-Oliver Stehr Specifying an Active Network Programming Language in Rewriting Logic: A Brief Overview ******************************************************************** This document gives a brief overview of our specification of PLAN, an active network programming language, in Maude, a formal specification language based on rewriting logic and membership equational logic. For an extended version with many more details we refer to doc-extended.txt. What are Active Networks ? ========================== "Active networks explore the idea of allowing routing elements to be extensively programmed by the packets passing through them. This allows computation previously possible only at endpoints to be carried out within the network itself, thus enabling optimizations and extensions of current protocols as well as the development of fundamentally new protocols." [http://www.cis.upenn.edu/~switchware/] Active networks are networks with nodes that do not operate according to a fixed scheme (e.g. as conventional routers) but are instead fully programmable and provide execution enviromments for programs that can be received from other other nodes via the network. An active network does not necessarily have a static topology, so that also unreliable, wireless and hybrid networks are subsumed by this notion. One may think of active networks as a generalization of conventional networks and as a step toward greater flexibility: Packets, which are interpreted by routers in conventional networks following rigid schemes, become programs, which are executed in active networks in a universal fashion. See [TeSmSiWeMi97] for a survey of active network research and the recent DARPA conference on this subject [DISCEX00]. What is PLAN ? ============== "PLAN is a resource-bounded functional programming language that uses a form of remote procedure call to realize active network packet programming. It is part of the SwitchWare Project." [http://www.cis.upenn.edu/~switchware/PLAN/] One of the central issues of active network research is the devlopment of programming paradigms which provide a suitable level of abstraction to develop active network applications. A particular programming language providing such a new paradigm is PLAN, the Packet Language for Active Networks [HiKaMoGuNe98a, HiKaMoGuNe98b, MoHiNe99, HiKe99, KaHiMoGu99], which has been implemented as part of PLANet, an active internetwork architecture [HiMoAlGuNe99]. PLAN is an imperative functional language similar to ML, but has a number of unique additional features, such as remote function execution, resource awareness and anytime typechecking. Remote function execution, means that functions can be applied to arguments so that the execution does not take place locally but in the execution enviromnent of a different network node. To this end, the function call is treated as a so-called chunk, i.e. as a piece of data, which is transmitted to the destination node by means of a packet. Resource awareness refers to a mechanism which keeps track of computational resources and ensures that all PLAN programs are terminating. In addition PLAN programs interact with their host nodes through Service Package interfaces. Basic services include provision of information about local network topology, local node properties, time, and routing. Additional possible services include resident data services for (time-limited) data storage and retrieval. For details we refer to the PLAN programmer's guide [HiMoKa01]. Semantics of PLAN in Maude ========================== We give an executable formal specification of PLAN using the lanugage Maude [maude-manual,maude-tutorial] which is based on a version of rewriting logic [Meseguer92] with a membership-equational sublogic [BoJoMe00-tcs]. The specification has been developed in a collaborative effort by Carolyn Talcott (Stanford Univerity), Mark-Oliver Stehr (SRI), Jose Meseguer (SRI), with support by the PLAN group, in particular Carl A. Gunter and Pankaj Kakkar (University of Pennsylvania) in the scope of the DARPA Active Network Program [DARPAAN] and the ONR Coordinated Research in Adaptive Network Centric Computing [ONRAN]. In accordance with a reseach objective which has been first set in [WaMeGu00] our work provides a formal semantics for PLAN. Indeed our specification fully captures the intent of the specifications [Kakkar99] and [KaGuAb00], but has the benefit of being both rigorously formal and executable. As shown in [Talcott01] our specification can be used as an active network model with execution environments for PLAN programs. More generally, a formal executable specification can be used at very different levels [DeMeTa00] ranging from formal modeling and execution via model-checking and narrowing analysis to formal verification. For instance, the use of abstract execution in this context is currently under investigation [Talcott01]. By exploiting the capabilities of rewriting logic, the Maude specification enhances the original PLAN specification in several aspects. For instance, the Maude specification directly reflects the concurrent nature of the network, meaning that each node makes only use of local information about the network topology and that the possibility of concurrent execution in different nodes is directly reflected in the specification. A particularly interesting aspect of the problem and our specification is the presence of {multilevel concurrency}: (1) A network configuration is modeled as a multiset containing nodes and packets. (2) With each node we associate a multiset of processes local to the node, which serve as execution environments for programs and can themselves execute concurrently within the node. (3) Each process encapsulates the local state of the execution environment together with an abstract reduction machine. To specify the abstract machine we use a general approach suitable for functional languages with side-effects which is inspired by [FeFr86,HoMaSmTa95,MaTa01]. The main idea is that the reduction state of the abstract machine is a pair, consisting of a reduction context (i.e. an expression with a hole, i.e. a metavariable) and the expression to be reduced in this context. Furthermore, the specification uses the CINNI calculus [Stehr00] to specify the binding structure of the language and to formalize environments as explicit substitutions. A particular benefit of this approach is that environments can always be eliminated, resulting in a specification that does not have to deal with them explicitly at various places. Especially the delicate issue of binding and environment handling in the context of recursive remote function calls turns out to have a very elegant solution. In summary, the use of the abstract reduction machine in connection with CINNI has greatly increased the clarity and reduced the complexity of the specification w.r.t. earlier versions [Stehr00-fmoods,Talcott00], bringing us closer to the goal of a specification which is useful for application programmers, language designers/implementors and formal methods researchers. Our specification uses a representation of programs based on an imperative lambda-calculus and presupposes that PLAN programs are mapped to this uniform representation by a simple preprocessing stage. For instance, in PLAN programs recursive references to functions can only occur inside the chunks which are arguments to Eval, OnNeighbor, or OnRemote; otherwise the termination property would be compromised. Part 1: The Active Network State -------------------------------- The overall state of the modelled active network is called a configuration. It is a multiset of objects which can be classfied as follows: 1. Each network node is represented by an object of sort Node with a constructor op Node : Loc AddrList ConnectionList RouteList -> Node which specifies the location (sort Loc), which serves as a node identifier (it could be a physical device, or simply an abstraction), the devices connecting the node to the network (sort AddrList), all connections to neighbors (sort ConnectionList), and the node's routing table (sort RouteList). Altogether all nodes in the configuration contain the information about the network topology. 2. Each process on a node is represented by an object of sort Process with a constructor op Process : Loc Addr Addr MachineInt MachineInt RedState -> Process which specifies the physical location (sort Loc), i.e. the node on which it is running, the originator address (sort Addr), i.e. the address of the application which injected the program (more precisely the initiating packet) into the network, the arrival device of program (Addr), i.e. the device at which it entered the current node, a session key (sort MachineInt), which is unique to each injected program, the resource bound (sort MachineInt), which specifies the remaining resources, and most importantly the reduction machine state (sort RedState), which contains the program (which may already be partially executed) and its current continuation state. Notice that there can be an arbitrary number of processes running at a single location, i.e. associated with a network node. 3. Each packet in transit between nodes is represented by an object of sort Packet with a constructor op Packet : Addr Addr Addr MachineInt MachineInt Const Val ValList -> Packet which specifies the final destination address (sort Addr) of the packet, the immediate destination address (sort Addr), i.e. the address of the next hop, the originator address (sort Addr), i.e. the address of the application which injected the program into the network, a session key (sort MachineInt), the resource bound (sort MachineInt), the routing function (sort Const), and the chunk which contains an invocation, i.e. a function (Val) with (evaluated) arguments (ValList). 4. A generator of fresh session keys is represented by an object of sort FreshKey with a constructor op FreshKey : MachineInt -> FreshKey . To ensure uniquenes of keys there should be only one such object in the configuration. 5. For the resident data services each node has an associated data object of sort Data with a constructor op Data : Loc DataItemList -> Data . which specifies the physical location (sort Loc), an list of data objects (sort DataItemList). Further Remarks: In the specification we identify each network device of a node with its network address (for example an IP address). As a consequence the PLAN types "Host" and "Dev" are represented by the type "Addr" of addresses. At moment there is no neighbor discovery mechanism or means for the set of neighbors to change. It shouldn't be hard to add this if/when it becomes interesting to do so. Part 2: The Transition Rules ---------------------------- When a packet arrives at its destination node a process is created to execute the invocation. The local execution of a process is specfied by an abstract reduction machine which explicitly keeps track of the context in which an expression is reduced. A Plan invocation is executed on an abstract reduction machine in the context of information contained in the packet (such as resource bound, source, address of arrival interface ...). All this information constitutes the state of a process (see above). The machine state (sort RedState) which is part of the process has a constructor op RedState : Cx Ex -> RedState which specifies the (functional) reduction context and the expression to be reduced. The purpose of the reduction machine is to perform execution of programs in a controlled way, since the order of execution is essential in an imparative language like PLAN (for instance, the resident data services provide a notion of storage). The configuration evolves by (1) rules for routing and delivering packets in transit Example: The service function "OnNeigbor" emits a packet. crl Node(l,devs,nbrs,rt) Process(l, orign, ariv, ssn, rb, RedState(cx, (OnNeighbor ((Chunk (val,vall)), (Addr dest),(Int int),(Addr dev))))) => Node(l,devs,nbrs,rt) Process(l, orign, ariv, ssn, (rb -int), RedState(cx, Dummy)) Packet(dest, dest, orign, ssn, (int - 1), DefaultRoute, val, vall) if contains(devs,dev) and contains(nbrs,(dev >> dest)) and (rb >= int) and (int > 0) . The current resource of the executing packed (rb) is decreased by the amount given to the emitted packet, and that amount is then decreased by one corresponding to the use of one unit for the first hop. Example: A packet received by a node may become a process. crl Node(l,devs,nbrs,rt) Packet(dest, fdest, orign, ssn, rb, rf, val, vall) => Node(l,devs,nbrs,rt) Process(l, orign, dest, ssn, rb, RedState(?,(val vall))) if (dest == fdest) and contains(devs,dest) . (2) rules for executing process steps which come in 4 flavors 2.1 reduction machine rules -- functional programming (rules that use only the reduction machine state) There are two kinds of reduction machine rules: 2.1.1 control rules, which focus on the next relevant redex and update the context accordingly. Example: A function is applied to a list of arguments. Arguments should be evaluated from left to right, i.e. the first non-value argument becomes the new focus. rl RedState(cx, (val (vall', nval', exl'))) => RedState(<< ? := (val (vall', ?, exl')) >> cx, nval') . 2.1.2 proper reduction rules, which perform the actual reduction without changing the context. Example: A lambda-abstraction is applied to a list of evaluated arguments. rl RedState(cx, ((Lam [idl : typel] ex) vall)) => RedState(cx, [idl := vall] ex) . In the righthand side of the rule [idl := vall] represents a substitution mapping elements of the IdList idl to corresponding to corresponding elements of the ValList vall. 2.2 process rules (rules that aditionally use the information in the process) Example: The service function "getRB" returns the resource bound of the current process. rl Process(l, orign, ariv, ssn, rb, RedState(cx, (GetRB empty-exl))) => Process(l, orign, ariv, ssn, rb, RedState(cx, (Int rb))) . 2.3 network service rules (rules that additionally use the information of the accociated node) Example: The service function "ThisHostIs" checks if a given address is a local address (i.e. a network device) of the node on which the current process is running. rl Node(l,devs,nbrs,rt) Process(l, orign, ariv, ssn, rb, RedState(cx, (ThisHostIs (Addr a)))) => Node(l,devs,nbrs,rt) Process(l, orign, ariv, ssn, rb, RedState(cx, (Bool (contains(devs,a))))) . 2.4 data service rules (rules that additioanlly use the resident data storage associated with the process) Example: The service function "Delete" removes a data item from the store associated with the current process. rl Data(l,dil) Process(l, orign, ariv, ssn, rb, RedState(cx, (Delete ((String str),(Key key))))) => Data(l,delete(dil,str,key)) Process(l, orign, ariv, ssn, rb, RedState(cx, Dummy)) . Delivery rules apply to packets whose next hop address is the destination address. In this case a process is created on the destination node to evaluate the packet. Routing rules apply to packets not yet at their destination.