Dynamic memory management for programmable devices.
The paper presents the design and implementation of a novel dynamic memory-management scheme for ESP---a language for programmable devices. The firmware for programmable devices has to be fast and reliable. To support high performance, ESP provides an explicit memory-management interface that can be implemented efficiently. To ensure reliability, ESP uses a model checker to verify memory safety.The VMMC firmware is used as a case study to evaluate the effectiveness of this memory-management scheme. We find that the Spin model checker is able to exhaustively verify memory safety of the firmware; the largest process took 67.6 seconds and used 34.45 Mbytes of memory to verify. We also find that the runtime overhead to maintain the reference counts is small; the additional overhead accounts for 7.35% of the total message processing cost (in the worst case) over a malloc/free interface.
INTRODUCTION
Traditionally, devices implement simple functionality that
is usually implemented in hardware. All the complex functionality
is implemented in device drivers running on the
main processor. However, as devices get faster, it is increasingly
harder for software running on the main CPU to keep
up with the devices. This is because the main CPU has to
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
ISMM'02, June 20-21, 2002, Berlin, Germany.
go across the memory and I/O buses to reach the device
and incurs several hundreds of cycles for each access. In
these situations, better performance can be achieved by implementing
some of the functionality on the device instead
of on the main CPU [2, 22, 9, 21, 18, 20, 25, 1, 24].
Programmable devices can be used to implement the increasingly
sophisticated functionality that has to be supported
by the devices. These devices are equipped with a
programmable processor and memory (Figure 1). Since the
processor resides on the card, it incurs a much smaller overhead
to access the control registers on the device.
Writing firmware for the devices is di#cult for two rea-
sons. First, the code running on the device has to be fast.
The processing power and memory on the device tends to
be at least an order of magnitude less than the main CPU
and the main memory. Migrating code from the main CPU
to the device involves a tradeo# between running the code
on a faster processor that incurs higher overhead to access
the device, and running it on a slower processor that has
faster access to the device. The slower the code runs on the
device, the smaller the benefit of migrating code to devices.
Second, device firmware has to be reliable, as it is trusted
by the operating system. It has the ability to write to any
location in the physical memory. A stray memory write resulting
from a bug can corrupt critical data structures in the
operating system and can crash the entire machine.
Firmware for programmable devices is usually written using
event-driven state machines in C. This is because concurrency
is an e#ective way of structuring firmware for programmable
devices; the multiple threads of control provide
a convenient way of keeping track of the progress of several
events at the same time. And event-driven state machines
support low-overhead concurrency. However, programming
with event-driven state machines in C su#ers from a number
of problems [17]. Consequently, while the device firmware
can deliver good performance, it is often di#cult to write
and debug.
ESP [17, 16] is a language for writing firmware for programmable
devices using event-driven state machines. It is
designed to meet three goals: ease of programming, ease of
debugging, and high performance.
This paper focuses on the novel memory-management scheme
supported by ESP. An earlier paper [17] included a brief
description of this scheme. This paper presents a detailed
description of design and implementation of ESP's dynamic
memory management scheme. This paper also provides detailed
measurements in VMMC firmware to evaluate the effectiveness
of our approach.
is challenging because the firmware has to be fast as well
as reliable. The problem is compounded by the fact that
the firmware is implemented using concurrency. Traditional
memory management schemes fall into two categories: automatic
and explicit memory management. On one hand, automatic
memory management using garbage collection techniques
[26] provides safety but usually involves high overhead
(both in terms of the amount of memory and processing
time). On the other hand, explicit memory management
involves lower overhead but is hard to program correctly.
Section 6 discusses the related work in more detail.
To keep the dynamic memory management overhead low,
ESP provides an explicit memory management interface.
It then uses a model checker (Spin [15]) to ensure memory
safety. The key observation is that allocation bugs are
di#cult to find because memory allocation correctness is a
global property of a program-the property cannot be inferred
by looking only at a single module of the program.
To rectify this, ESP is designed to make memory allocation
correctness a local property of each process. This not
only promotes modular programming but also allows model
checkers to verify safety. This is because model checking involves
an exponential search. Making memory safety a local
property results in smaller models that are more amenable
to model checking.
The ESP runtime maintains reference counts on objects
to manage the dynamic allocation e#ciently. To make memory
allocation correctness a local property of each process,
objects sent over channels are passed by value in ESP. Se-
mantically, this means that a copy of the object being sent
over a channel is delivered to the receiving process. This
ensures that no two processes share an object. However,
copying objects being sent over channels at runtime can
be expensive. The ESP runtime avoids copying objects by
maintaining reference counts on objects so that the objects
are actually shared by multiple processes under the covers.
To demonstrate the e#ectiveness of our approach, we use
the VMMC firmware as a case study. The VMMC firmware
runs on the Myrinet [4] network interface cards and was programmed
using ESP. We found that the Spin model checker
was able to exhaustively verify memory safety of each of
the ESP processes in the VMMC firmware implementation.
The largest process took 67.6 seconds and 34.45 Mbytes of
memory to verify. We also found that the reference counting
used by the ESP runtime incurs a fairly small overhead.
Our measurements indicate that the additional bookkeeping
necessary to maintain the reference count results in a 7.35 %
increase (in the worst case) in message processing cost over
a malloc/free interface that is supported by C.
The rest of this paper is organized as follows. Section 2
presents a brief introduction to model checking. Section 3
presents an overview of ESP. Section 4 describes the design
and implementation of ESP's dynamic memory management
scheme. Section 5 uses the VMMC firmware to evaluate the
e#ectiveness of our scheme. Section 6 discusses the related
work. Finally, Section 7 presents our conclusions.
2. BACKGROUND
ESP uses model checkers to debug and extensively test the
device firmware. Model checking is a technique for verifying
a system composed of concurrent finite-state machines.
Given a concurrent finite-state system, a model checker ex-
CPUCPU
BUS
Main Memory
Main CPU
Network
DMA
DMA
CPU
MEM Card
Network
DMA
CPU

Figure

1: A machine with programmable devices
plores all possible interleaved executions of the state machines
and checks if the property being verified holds. A
global state in the system is a snapshot of the entire system
at a particular point in execution. The state space of the
system is the set of all the global states reachable from the
initial global state. Since the state space of such systems
is finite, the model checkers can, in principle, exhaustively
explore the entire state space.
Model checking verifiers can check for a variety of prop-
erties. These properties are traditionally divided into safety
and liveness properties. Safety properties are properties that
have to be satisfied in specific global states of the system.
Assertion checking and deadlock are safety properties. Assertions
are predicates that have to hold at a specified point
in one of the state machines. This corresponds to the set
of global states where that state machine is at the specified
point and the predicate holds. A deadlock situation corresponds
to the set of all the global states that do not have a
valid next state. Liveness properties are ones that refer to
sequence of states. Absence of livelocks is a liveness property
because it corresponds to a sequence of global states where
no useful work gets done. Liveness properties are usually
specified using temporal logics.
The advantage of using model checking is that it is auto-
matic. Given a specification for the system and the property
to be verified, model checkers automatically explore the
state space. If a violation of the property is discovered, it
can produce an execution sequence that causes the violation
and thereby helps in finding the bug.
The disadvantage of using model checking is that it is
computationally expensive. The state space to be explored
is exponential in the number of processes and the amount
of memory used by the program. As a result, the resources
required (CPU as well as memory resources) by the model
checker to explore the entire state space can quickly grow
beyond the capacity of modern machines.
3. ESP
The Event-driven State-machines Programming (ESP) [17,
16] is a language for programmable devices. It is designed to
three goals: ease of programming, ease of debugging,
and high performance.
In this section, we begin with a description of the approach
ESP takes to meet its goals. We then present an overview
of the ESP language.
3.1 Approach
ESP meets its three goals as follows (Figure 2):
Ease of programming. To support ease of programming,
ESP allows programs to be expressed in a concise modular
fashion using processes and channels. In addition, it provides
a number of features including pattern matching to
support dispatch on channels, a flexible external interface
to C, and a novel memory management scheme that is e#-
cient and safe.
Ease of debugging. To support ease of debugging, ESP
allows the use of a model checker like Spin [15] to extensively
test the program. The ESP compiler (Figure 2) not only
generates an executable but also extracts Spin models from
the ESP programs [16]. This minimizes the e#ort required in
using a model checker to debug the program. Often, the ESP
program is debugged entirely using the model checker before
being ported to run on the device. This avoids the slow and
painstaking process involved in debugging the programs on
the device itself.
High performance. To support high performance, the ESP
language is designed to be fairly static so that the compiler
can aggressively optimize the programs. In languages like
C, event-driven state machines are specified using function
pointers. This makes it di#cult for the C compiler to optimize
the programs. This forces the programmers to hand
optimize the program to get good performance. In contrast,
ESP is designed to support event-driven state machines. It
allows the ESP compiler to generate e#cient code.
3.2 Language Overview
The ESP language adopts several structures from CSP [14]
and has a C-style syntax. ESP supports event-driven state-machines
programming.
Concurrency in ESP is expressed using processes and chan-
nels. An ESP program consists of a set of processes communicating
with each other over channels. Each process represents
a sequential flow of control in the concurrent program
and implicitly encodes state machines.
Processes communicate with each other over channels.
Messages are sent over the channel using the out operation
and received using the in operation. Communication
over channels is synchronous 1 or unbu#ered-a process has
to be attempting to perform an out operation on a channel
concurrently with another process attempting to perform an
in operation on that channel before the message can be successfully
transferred over the channel. Consequently, both in
and out are blocking operations. The alt statement allows a
process to wait on in and out operations on several di#erent
channels till one of them becomes ready to complete.
In addition to basic types like int and bool, ESP supports
mutable and immutable versions of complex data types like
record, union and array. However, ESP does not support
recursive data types for two reasons. First, specification
languages for model checkers do not support recursive data
types. sending recursive data types by-value over
channels involves additional run-time overhead.
In ESP, processes and channels are static and are not first-class
objects-they can neither be created dynamically nor
Also known as rendezvous channels.
stored in variables nor sent over other channels. This design
allows the compiler to perform optimizations more effectively

ESP supports pure message passing communication over
the channels. Allowing processes to communicate over shared
memory (using shared mutable data structures) would require
ESP to provide additional mechanism (like locks) to
avoid race conditions. To avoid this, ESP does not allow
processes to share data structures.
Two aspects of ESP prevent sharing of data structures.
First, ESP disallows global variables. Each variable is local
to a single process. Second, objects sent over channels are
passed by value. To support this e#ciently, ESP allows only
immutable objects to be sent over channels. This applies not
only to the object specified in the out operation but also to
all objects recursively pointed to by that object.
4. DYNAMICMEMORYMANAGEMENTIN
4.1 Design
The design of the memory management scheme in ESP
was driven by two goals. First, the programs should be
safe. Bugs stemming from lack of safety are di#cult to find.
The problem is compounded by the fact that these programs
are concurrent and run on devices with minimal debugging
support. Second, the memory management overhead has to
be small.
ESP provides a novel memory management scheme that
provides safety as well as low overheads. To manage dynamically
allocated memory, it provides an explicit malloc/free-
style interface that incurs low overheads. It ensures safety
using a model checker. The only unsafe aspect of ESP is its
explicit memory management scheme. The memory allocation
bugs are eliminated using a model checker. This results
in safe ESP program that incur low memory-management
overhead at runtime.
The key observation is that allocation bugs are di#cult
to find because memory allocation correctness is a global
property of a program-the property cannot be inferred by
looking only at a single module of the program. A programmer
has to examine the entire program to make sure that all
allocated objects are eventually freed and are not accessed
once freed.
To rectify this, ESP makes memory allocation correctness
a local property of each process. Section 3.2 describes the
design choices that ensure that no two processes share any
data structure. It should be noted that to support pure
message passing-style communication, it would have been
su#cient to ensure that no two processes share any mutable
data structures. However, to make memory allocation
correctness a local property, ESP disallows sharing of even
immutable data structures.
Making memory allocation correctness a local property allows
the model checker to verify the memory safety of each
process separately. The ability to check each process separately
ensures that the size of model to be checked remains
small. The largest model that has to be checked depends
only on the size of the largest process and not on the size
of the entire program or the number of processes. Con-
sequently, we were able to exhaustively check the memory
safety of all ESP processes in the VMMC firmware (Sec-
pgm.ESP ESP Compiler
pgm.C help.C Generate Firmware
using C Compiler
pgmN.SPIN
Verify Property 1
Verify Property N
using SPIN
using SPIN

Figure

2: The ESP approach. The ESP compiler generates models (pgm[1-N].SPIN) that can be used by the Spin
model checker to debug the ESP program (pgm.ESP). The compiler generates three types of models: detailed (retains all the
details in the program), memory-safety (to check memory safety), and abstract (to generate more compact model by dropping
some irrelevant details). The compiler also generates a C file (pgm.C) that can be compiled into an executable. The shaded
regions represent code that has to be provided by the programmer. The test code (test[1-N].SPIN) is used to check di#erent
properties in the ESP program. It includes code to generate external events such as network message arrival as well as to
specify the property to be verified. The programmer-supplied C code (help.C) implements simple low-level functionality like
accessing special device registers, dealing with volatile memory, and marshalling packets that have to be sent out on the
network.
tion 5.2). In addition, making memory allocation correctness
a local property promotes modular programming.
Objects sent over channels are passed by value. The
means that a deep copy of the object is delivered to the receiving
process. 2 Objects received over a channel are treated
like newly allocated objects and have to be later freed by
that process. One possible complication occurs when an object
contains multiple links to another object. If pointer
sharing were preserved, the receiving process would need to
know about the sharing to check that the data structure was
correctly freed. However, it cannot determine the sharing
because pointer comparisons are not allowed in ESP. The
example in Figure 3 illustrates the problem with copying
semantics that preserves pointer sharing.
To avoid this, the deep copy performed when a data structure
is sent over a channel does not preserve pointer sharing.
This allows a receiving process to simply perform a recursive
arriving over channels.
ESP provides a malloc/free-style interface to manage dynamically
allocated memory. Since objects are not shared
between the processes, each process is responsible for freeing
its objects. Two primitives (free and rfree 3 ) allow
processes to free the allocated objects. In addition, ESP
provides two other primitives(pfree and prfree) which free
the object after evaluation of the current expression. This
allows the compiler to perform an optimization (Section 4.3).
The following code fragment
out( chan1, prfree(v));
is equivalent to
out( chan1, v);
ESP supports immutable as well as mutable data struc-
tures. An immutable object arriving on a channel can be
2 This is true only semantically. The ESP runtime never has
to actually copy objects sent over channels (Section 4.3).
3 which performs free recursively
mutated by first applying a cast operation to obtain a mutable
version of the object. Semantically, the cast operation
causes a new object to be allocated and the corresponding
values to be copied into the new object. However, the compiler
can avoid creating a new object in a number of cases.
For instance, if the compiler can determine that the object
being cast will be freed immediately after the cast, it can
reuse that object and avoid allocation.
ESP allows dangling pointers (pointers to objects that
have been already freed) during program execution. If dangling
pointers were not allowed, the program would have to
delete all pointers to a given object before that object could
be freed. This would require additional bookkeeping and
would place unnecessary burden on the programmer. Although
ESP allows dangling pointers, it disallows the use
of these pointers to access memory. This ensures memory
safety. In contrast, the usual approach to ensure memory
safety is to reclaim an object only if no pointers point to it.
This avoids dangling pointers. The only other approach that
we are aware of that provides safety while allowing dangling
pointers is region-based memory management [19]. It uses
the type system to guarantee that the dangling pointers are
not used at run time.
Memory allocation in ESP is a nonblocking operation. In
a concurrent program, making memory allocation blocking
has some advantages. It allows a memory allocation request
in one process that does not find any memory available
to block till another process frees up some memory.
Although this would lead to better memory utilization, it introduces
additional synchronization between the processes.
This forces the programmer to treat each allocation as potentially
blocking and make sure that it does not cause the
program to deadlock.
4.2 Extracting Memory-Safety Models
Currently, ESP used the Spin model checker [15]. Spin is
a flexible and powerful model checker designed for software
systems. Spin supports high-level features like processes,
rendezvous channels, arrays and records. Most other ver-
record of { v: int}
channel shareC: array of entryT
process process1 {
in( shareC, $a);
assert( length(a) == 2);
process process2 {
{ 11 };
out( shareC, { -> p1, p2});
process process3 {
{ 5 };
out( shareC, { -> p, p});

Figure

3: An example to illustrate the problems with copying semantics that preserves pointer sharing.
Process process1 expects an array of two elements on the channel shareC. Once it receives it, the process frees one of the
entries and proceeds to use the other entry. If process process2 sends an array on the channel, process1 would execute
correctly because the two entries point to di#erent objects. However, if process process3 sends an array on the channel,
process1 will try to access the record after it has freed it resulting in an error.
ifiers target hardware systems and provide a fairly di#er-
ent specification language. Although ESP can be translated
into these languages, additional state would have to be introduced
to implement features like the rendezvous channels
using primitives provided in the specification language. This
would make the state explosion problem worse. In addition,
the semantic information lost during translation would make
it harder for the verifiers to optimize the state-space search.
allows verification of safety as well as liveness prop-
erties. The liveness properties in Spin are specified using
Linear Temporal Logic (LTL).
The ESP compiler generates three types of models: de-
tailed, memory-safety, and abstract [16]. The detailed models
contain all the details from the original ESP program.
These models are useful during the development and de-bugging
of the firmware using the simulation mode in Spin.
The memory-safety models are used to check for memory allocation
bugs in the program. These models are essentially
detailed models with some additional Spin code inserted to
check for validity of memory accesses. The abstract models
omit some of the details that are irrelevant to the particular
property being verified. These models can have significantly
smaller state than the detailed models and are useful for
checking larger systems. In this paper, we will discuss in
detail only the memory-safety models.
The memory-safety models generated by the ESP compiler
can be used to check for memory allocation bugs in
the program. These models are essentially detailed models
with some additional Spin code inserted to check for validity
of memory accesses. Therefore, they contain even more
state than the detailed models. In spite of this, these models
can be usually used to exhaustively explore the state space
for allocation bugs. This is because the memory safety of
each individual process can be checked separately using the
verifier (Section 4.1).
Variables in ESP store pointers to data objects. For in-
stance, in the following code, variables b1 and b2 point to
the same array. Therefore, the update (b1[1]) should be
visible to variable b2.
$b1: #array of int = #{ -> 5, 11}; // Allocate
Since Spin does not support pointers, each object in the
generated model is assigned an objectId at allocation time.
The objectId is stored as an additional field in the object
itself. When an object gets copied due to an assignment
operation, the objectId field also gets copied. This ensures
that all objects in the translated Spin code that share the
same objectId represent a single object in the original ESP
code. When a mutable object gets updated in ESP code,
the translated Spin code includes code to check and update
all other objects with the same objectId.
The memory-safety model includes additional code (asser-
tions) that checks the validity of each object that is accessed.
When a new object is allocated, an unused objectId is assigned
to the object. Before every object access, code is
inserted in the model to check that the object is live. Array
accesses include additional code to check that the array
index is within bounds. Union references include code to
check that field being accessed is valid. When an object is
all objects in the model with that same objectId are
marked as invalid by changing the objectId field to -1.
The memory-safety model checks for bugs like accessing
an object after it has been freed, double freeing an object,
and using an invalid array index. In addition, it can also
find most memory leaks. This is because a process in the
generated model has a bounded number of objects and the
compiler can determine this bound. Arrays are the only
source of unbounded allocation in an ESP process, since
ESP does not support recursive data types. However, the
ESP compiler imposes a bound on the maximum lengths of
the arrays during model extraction [17], thereby bounding
the number of objects in the model. By constraining the
model to only pick objectIds within this bound, any steady
memory leak can be detected. A steady leak will cause the
model to run out of objectIds during model checking.
Currently, the objectIds are a source of unnecessary increase
in state space to be explored in models generated by
the ESP compiler. The problem stems from the fact that a
given object in the program can get assigned di#erent objectIds
depending on the scheduling decisions made prior
to its allocation. The result is that a single "state" manifests
itself as several di#erent states in the state space. This
problem can be alleviated by using a separate objectId table
for each distinct type in each process. This is because
two pointers can point to the same object only if they have
the same type and belong to the same process. This should
reduce the number of di#erent objectIds a given object can
get assigned.
4.3 Code Generation
From the programmer's perspective, each process has its
own set of objects that have to be managed separately for
each process (Section 4.1). Each process allocates its objects
and explicitly frees them (using free). Objects sent
over the channels are deep copied before being handed to
the receiving processes. Therefore, objects arriving over a
channel are treated like newly allocated objects that have
to be later freed by that process.
The implementation uses a reference-counting scheme to
manage the objects. Although semantically, processes do
not share objects, the implementation shares objects between
processes for e#ciency-copying objects is computationally
expensive. The runtime system maintains reference
counts to keep track of the number of processes sharing
the object. Recursive increment and decrement operations
on cyclic data structures require additional bookkeeping to
avoid infinite loops. However, ESP does not support recursive
data types. Consequently, these operations can be
implemented e#ciently.
Normal allocation causes objects to be allocated and their
reference count initialized to one. When an object is sent
over a channel, the reference count of the object is recursively
incremented (thereby avoiding the expensive deep copy
before giving it to the receiving process. When
a process frees an object, its reference count is decremented
by one. The object is actually deallocated only when all the
processes have freed it and the reference count is zero.
The following simple optimization is fairly e#ective in reducing
the number of reference count increments and decre-
ments. In the following code fragment
out( chan1, prfree(v));
the reference count will be recursively incremented before
sending the object v on the channel. After sending the
object, the reference count will be recursively decremented
because of the prfree. In this case, the reference count
increments and decrements can be optimized away by the
compiler.
The deep copy performed when a data structure is sent
over a channel does not preserve pointer sharing (Section 4.1).
This has two benefits. First, it allows the copying semantics
to be implemented e#ciently; a simple recursive increment
of reference count su#ces. An object that is pointed to multiple
times within the data structure will have its reference
count incremented multiple times. Second, it allows the correctness
of the memory allocation to be a local property of
each process (Section 4.1). The receiving process does not
have to worry about the pointer sharing on objects arriving
over channels.
A cast of an immutable object into a mutable object can
require copying the object. This is because a program can
detect object sharing by mutating it at one location and
observing the change at another location. However, the cast
operation is fairly uncommon in ESP programs. In addition,
the copying is not always necessary. The copy can be often
avoided when a cast is necessary but the program is written
carefully (to allow the compiler to optimize it). For instance,
if the reference count of the immutable object is one (no
other process is holding that object) and the object is freed
immediately after the cast, the compiler can avoid the copy
and use the same object.
record of { v: int}
channel countC: array of entryT
process processA {
{ 3 };
{ -> p1, p2};
out( countC, a);
process processB {

Figure

4: An example that shows that the traditional
reference counting scheme is not su#cient for
ESP.
Several design choices in the ESP language allow the implementation
to share objects while providing the illusion
of the disjoint set of objects. First, only immutable objects
can be sent over channels. Therefore, the program cannot
detect that the object is being shared by mutating it in one
process and observing the change in another process. Sec-
ond, objects cannot be compared for pointer equality. This
prevents the program from comparing the pointer for two
di#erent objects and detecting that the implementation is
using the same object to represent both of them. Finally,
ESP does not support recursive data types, and therefore
the program cannot have cyclic data structures. This means
that recursive reference count increments does not have to
deal with infinite loops due to cyclic data structures, and
can therefore be implemented e#ciently.
Traditional reference counting schemes maintain the counts
on the objects di#erently from the way it is done in ESP. In
the traditional scheme, the reference counts are incremented
only at the root and decremented recursively only when the
reference count of the object becomes zero. Our earlier paper
[17] suggested that this would be su#cient for ESP too.
It turns out that this is not su#cient. Consider the example
in

Figure

4. Until the point when the objects are sent over
the channel countC, both schemes would have kept the same
reference counts on all the objects; each of the three objects
(pointed to by the variables p1, p2, and a) would have a
reference count of one. However, on performing the send
operation on the channel countC, the traditional scheme will
increment the reference count of only the array object while
the ESP scheme will increment the reference count of each
of the three objects. If the scheduler chooses to schedule
the process processB first, then the free statement will be
executed. With the traditional scheme, this will cause the
reference count of the object pointed to by p1 to go to zero,
thereby freeing the object. This will generate an error when
the process processA is scheduled to run and it tries to access
the variable p1. With the ESP scheme, the reference
count of the object pointed to by p1 will be decremented
from two to one, and so the object will not be freed. This
allows the process processA to later access it.
4.4 Limitations
One of the main limitations of this approach is that it has
problems dealing with recursive data types. The problem is
that recursive data types introduce cyclic data structures. In
the presence of cyclic data structures, the deep copy semantics
of ESP does not make any sense. One possible approach
is to allow only noncyclic data structures on channels. This
might require additional checks at run time. However, these
checks would be necessary only on channels that allow recursive
data types.
5. EXPERIMENTAL RESULTS
This section presents measurements to demonstrate the
e#ectiveness of ESP's memory management scheme. The
measurements were performed on the VMMC firmware that
runs on the Myrinet [4] network interface cards. Our measurements
are designed to investigate the following issues:
. The programmer e#ort required to verify memory safety.
. The e#ectiveness of using the model checker to verify
memory safety.
. The extra performance overhead incurred at runtime
to maintain reference counts.
. The allocation pattern exhibited by the firmware. In
particular, we measure the object lifetimes.
Before answering these questions, this section presents a
brief overview of the VMMC firmware.
5.1 VMMC Firmware
The Virtual Memory-Mapped Communication (VMMC)
architecture [9] delivers high performance on gigabit networks
by using sophisticated network cards. It allows data
to be directly sent to and from the application memory
(thereby avoiding memory copies) without involving the operating
system (thereby avoiding system call overhead). The
operating system is usually involved only during connection
setup and disconnect.
The VMMC implementation [9] uses the Myrinet [4] net-work
interface cards. Myrinet is a packet-switched gigabit
network. The Myrinet network card is connected to the net-work
through two unidirectional links of 160 Mbytes/s peak
bandwidth each. The actual node-to-network bandwidth
is usually constrained by the PCI bus (133 Mbytes/s) on
which the network card sits. The network card has a programmable
memory and three DMA engines to transfer data- one to
transfer data to and from the host memory; one to send data
out onto the network; one to receive data from the network.
The card has a number of control registers including a status
register that checks for data arrival, watchdog timers
and DMA status.
The VMMC software (Figure 5) has three components: a
library that links to the application; a device driver that is
used mainly during connection setup and disconnect; and
firmware that runs on the network card. Most of the software
complexity is concentrated in the firmware code, which
was implemented using event-driven state-machines in C.
Significant e#ort [10, 9, 3, 6] has been spent on imple-
menting, performance tuning, and debugging the VMMC
Card
Interface
Processor
Main
Network
Application
Network
Firmware
Device Driver
Library

Figure

5: VMMC Software Architecture. The shaded
regions are the VMMC components.
Process ESP Generated Test
Program Model Code
reliableSend
reliableRecv 152 664 41
localReq 172 742 67
remoteReq 167 882 85
remoteReply 177 715 104

Table

1: Sizes (in lines) of the various files used
to check memory safety of the various processes in
the VMMC firmware. The three remaining processes
are not listed in the table because they did not involve any
allocation. The second column shows the size of the portion
of program relevant for the particular model. The third
column shows the size of the model generated by the ESP
compiler. The last column shows the number of lines of Spin
test code that was required.
firmware. In spite of this, we continue to encounter bugs in
the firmware.
The VMMC firmware was reimplemented using ESP. The
ESP version of the VMMC firmware required significantly
fewer lines of code than the C version. The ESP version
has 500 lines of ESP code together with around 3000 lines
of C code. All the complex state machine interactions are
restricted to the ESP code, which uses 8 processes and 19
channels. The C code performs only simple operations like
packet marshalling and handling device registers. This is a
significant improvement over the C version where the complex
interactions were scattered throughout the 15600 lines
of code.
5.2 Verifying Memory Safety in VMMCFirmware
The ESP compiler extracts memory-safety models that
can be used to verify the safety of each of the processes separately
(Section 4.2). To use these models to verify safety
involves two steps. First, the programmer has to provide
test code (test[1-N].SPIN in figure 2) to check each of the
processes. Then, the model checker is used to perform a
state-space exploration to verify safety. The former involves
programmer e#ort while the latter is performed automatically
and is constrained by the available computational resource

Programmer e#ort required. The test code for checking
memory safety has to be provided by the programmer
simulates external events such as network message arrival.
Unlike with other models, the test does not have to include
any additional code to check the safety-the code to check
for memory safety is included in the generated model in the
form of assertions. Table 1 presents the sizes of the test
code that had to be written to verify memory safety in the
firmware. 4 In each case, the size of the test code is
fairly small. The table also shows the size of the relevant
portion of the ESP code and the size of the models generated
by the ESP compiler.
Each test code has to be written only once but can be used
repeatedly to recheck the system as the software evolves.
Since the models are extracted automatically, rechecking the
software requires little programmer e#ort.
E#ectiveness of model checking. For every process in
the VMMC firmware, the entire state space could be explored
exhaustively using Spin. Table 2 presents the amount
of state that had to be explored to verify memory safety of
each of the processes. The biggest process (reliableSend)
required only 67.6 seconds of processor time and 34.45 Mbytes
of memory. This shows the e#ectiveness of the model checker
to verify safety.
This is in contrast with our experience with checking the
VMMC firmware for global properties like deadlocks [16].
The ESP compiler used abstraction techniques to generate
smaller models that would require less resource to explore
the state space. This approach allowed the model checker to
identify several hard-to-find bugs in the firmware that can
cause the firmware to deadlock. However, the state space
was still too big. As a result, Spin could only perform a
partial search due to resource constraints. This illustrates
the importance of making memory safety a local property
of each process.
The memory-safety model generated by the ESP compiler
catches not only all bugs due to invalid memory accesses but
also most of the memory leaks (Section 4.2). The memory
safety bugs in the VMMC firmware had already been eliminated
by the time the ESP compiler was modified to support
the memory-safety models. Spin was used to check an
earlier version of the firmware that had an allocation bug.
The verifier easily identified the bug. To further check the
e#ectiveness of using the memory-safety models, a variety
of memory allocation bugs were inserted manually in the
program. These bugs either access objects after they were
freed or use an invalid array index or introduce memory
leaks. Spin was able to quickly find the bug in every case.
In ESP, the model checker was used throughout the program
development process. Traditionally, model checking
is used to find hard-to-find bugs in working systems. Since
developing firmware on the network interface card involves
a slow and painstaking process, we used the Spin simulator
to implement and debug it. Once debugged, the firmware
was ported to the network interface card with little e#ort.
5.3 Performance
Reference counting overhead. We measure the performance
overhead incurred by the ESP runtime to manage
dynamic memory in the VMMC firmware. To put the over-
4 The processes not listed in the table did not involve any
dynamic allocation.
head in perspective, it estimates the additional overhead the
ESP's scheme would incur over a malloc/free interface that
is supported by C.
VMMC provides two types or operations to transfer data
between two machines. The remote-write operation transfers
data from the local machine to a remote machine. The
remote-read operation fetches data from a remote machine
to the local machine. A remote-read operation behaves like
two remote-write operations. It requires two messages to be
sent over the network-a request message sent by the local
machine and a reply message (with the requested data) sent
by the remote machine. Therefore, in this section, we report
only the measurements from the remote-write operations.
Measuring the memory management overhead on the firmware
poses a problem. The granularity of the clock available on
the Myrinet network card is fairly large (0.5 -s). There-
fore, we cannot simply instrument the firmware to measure
the fraction of time spent in the memory management rou-
tines. Consequently, we estimate the memory management
overhead in three steps.
First, we measure the overhead of each of the memory
management operations (second column in Table 3). When
a reference count decrement operation is performed, the object
is freed or not depending on whether the reference count
is zero. Therefore, the overhead in the both cases is mea-
sured. The overhead of all the memory management operations
should have little variance. This is because ESP uses
a simple scheme to manage the free memory. It keeps a set
of list of free blocks-all blocks in a particular list have the
same size. Consequently, allocating (or freeing) an object
involves removing from (or adding to) the head of a list.
Second, we measure the number of times each of these operations
is executed on a remote-write operation (Table 3).
Using the numbers from these two steps, we estimate the
memory management overhead involved in each remote-write
operation.
Finally, we instrument the VMMC firmware to measure
the total time spent to process each remote-write request
(third column in Table 4). Then we compute the fraction of
the total processing time spent in managing dynamic memory

Table

4).
ESP performs a common optimization performed by reference-counting
systems. The reference counts of newly allocated
objects are set to zero instead of one. Free objects are identified
by their presence in a free list. This avoids the need
for incrementing the counter before allocation and decrementing
it before freeing. Consequently, the actual cost of
maintaining the reference counts (Table 4) can be obtained
by adding the execution times in rows two and three in Table
3.

Table

4 shows that the overhead of maintaining the reference
is a fairly small fraction of the total memory-management
cost (27.7 % in the worst case). This is because very few reference
count increments (and decrements) were necessary in
the firmware. Only one reference count increment was necessary
on the sending side and only three on the receiving
side (

Table

3). The remaining memory management overhead
is the cost of allocating and freeing memory. This cost
would be incurred even by a simple malloc/free interface
provided in C.
One advantage of an explicit memory management scheme
is that the programmer can control when an object is freed.
This allows the programmer to get better performance by
Process Name No. of States Time (in Seconds) Memory Used (in Mbytes)
Stored Matched Stack Hash table States Store Total
reliableSend 11118 316725 67.6 24.0 1.0 9.45 34.45
localReq
remoteReq 2315 3510 0.9 24.0 1.0 1.87 26.87
remoteReply 8565 7312 2.3 24.0 1.0 5.55 30.55

Table

2: Checking for memory safety in the VMMC firmware using Spin. In each case, the entire state space
was explored in the exhaustive mode in Spin. The stored column shows the number of unique states encountered while the
matched column shows the number of states encountered that had already been visited before. The memory usage is broken
down into space used for the stack, the hash table, and the visited states. The space used by the stack and the hash table
are statically allocated by Spin.
Operation Operation Sender Receiver
Execution Time Operation Count Execution Time* Operation Count Execution Time*
Allocation 0.59 -s 3 1.77 -s 3 1.77 -s
Increment Ref Count 0.15 -s 1 0.15 -s 3 0.45 -s
Decrement Object not freed 0.26 -s 1 0.26 -s 3 0.78 -s
Count Object freed 0.48 -s 3 1.44 -s 3 1.44 -s
Total - 3.62 -s - 4.44 -s

Table

3: Estimate of the memory management overhead in the VMMC firmware. The table computes
the amount of time spent in the memory management primitives in the firmware when a machine sends a
message to another machine. It shows the time spent on both the sending as well as the receiving machines.
*These values were computed using the measurements in the other columns.
Machine Total Memory Management Overhead Reference Counting Overhead
Execution Time Execution Time % of Total Execution Time % of Total
Sender Small 19.50 -s 3.62 -s 18.56 % 0.41 -s 2.10 %
Rest 28.47 -s 3.62 -s 12.72 % 0.41 -s 1.50 %
Receiver 16.74 -s 4.44 -s 26.52 % 1.23 -s 7.35 %

Table

4: Comparison of the memory management overhead with the total time spent by the VMMC firmware
to process a message being sent over the network (both on the sender and the receiver machines). Since
messages of up to 32 bytes are treated di#erently than larger messages on the Sender, the overheads are shown separately for
the two categories: Small (<= bytes messages) and Rest. The total execution time was measured by instrumenting the
firmware. The memory management overheads were obtained from Table 3. The reference counting overhead is the overhead
of maintaining the reference counts in the object. It is obtained by adding the execution times in rows two and three in

Table

3.
Application Problem Size
LUContiguous 2048 x 2048 Matrix
WaterSpatial 15625 Molecules
BarnesSpatial 8192 Particles
WaterNsquared 1000 Molecules
Volrend head

Table

5: SPLASH2 Applications
moving some of the allocation overhead out of the critical
path.
Object lifetimes. We measure the lifetime of the allocated
objects in the VMMC firmware using SPLASH2 applications

Table

5). These applications run on top of the
Shared Virtual Memory (SVM) [3] library that, in turn, runs
on top of the VMMC library. All applications measurements
were made using a cluster of four SMP PC. Each PC
has four 200 MHz Pentium processors, 1 GB memory and a
Myrinet network interface card with a LANai 4.x 33 MHz
processor and 1 MB on-board SRAM memory. The nodes
are connected by a Myrinet crossbar switch. The PCs run

Table

6 shows the lifetimes of the objects allocated in the
firmware. The lifetime is measured in the number of allocations
and not the execution time. During each allocation,
a counter is incremented. As can be seen from the table,
most objects are freed very quickly-over 99 % of objects
are freed within 128 allocations. A small number of tables
are allocated when the firmware is started. These objects
are never freed.
6. RELATED WORK
Explicit Memory Management. Traditionally, dynamic
memory on programmable devices is managed using an interface
that allows the program to allocate and free memory
maintained in bu#er pools. When required, the programmer
explicitly maintains reference counts on the objects. These
interfaces do not provide memory safety. They often result
in memory allocation bugs that are notoriously di#cult
to find; they lead to memory corruption that manifests as
faulty behavior at a location in the program di#erent from
the site of the bug.
A number of tools [5] use static and runtime techniques
to find memory allocation bugs in unsafe languages like C.
For instance, the Purify [13] tool inserts code in the executable
that check for a number of bugs like invalid indices
in array accesses and memory leaks. This allows it to detect
an error when it happens at run time. However, it is the
programmer's responsibility to run the executable with different
inputs so as to exercise every possible program path.
LCLint [11] combines static analysis with program annotations
to identify a broad class of allocation bugs. A different
approach [23] to find a more limited class of bugs
(bu#er overruns) is to formulate the bu#er overrun problem
as an integer constraints problem and statically check
for constraint satisfaction. A limitation of these static approaches
is that it can flag false-positive as well as false-negative
bugs.
Automatic Memory Management. Automatic memory
management in safe programming languages is implemented
using a garbage collector that is responsible for reclaiming
unused memory [26]. Garbage collection often involves run-time
overhead (both in terms of processor overheads as well
as additional memory requirement) that make them di#cult
to use in programmable devices. Copying garbage collectors
usually use only half of the available memory. This is
a problem on programmable devices which have relatively
small amounts of memory. Mark-and-sweep collectors do
not waste memory but incur overhead proportional to the
size of the heap. Although some techniques [7] can be used
to reduce the cost during during the sweep phase, even the
cost during the mark phase can be significant. This is because
the firmware maintains a few large tables that have
to be scanned during the mark phase. This is a problem
on programmable devices where the collector would be triggered
frequently because of the limited memory available.
Memory Management using Regions. Vault [8] and
Cyclone [12] use regions [19] to provide safe memory man-
agement. Region-based memory management techniques
exiting dynamic contexts like procedures.
This makes them unsuitable for a language like ESP that
does not have any dynamic context.
7. CONCLUSIONS
This paper presented the design and implementation of
a novel memory-management scheme for ESP. ESP provides
an explicit interface to manage dynamic memory. This
interface can be implemented e#ciently using a reference-counting
technique. ESP's design makes memory-allocation
correctness a local property of each process. This allows a
model checker to be used to ensure the safety of the pro-
gram. This approach results in safe programs that incur
low runtime overheads to manage the memory.
The e#ectiveness of ESP's scheme was evaluated using the
VMMC firmware as a case study. We found that the Spin
model checker is able to exhaustively verify memory safety of
each of the ESP processes in the firmware. Verifying memory
safety took between 0.1 and 67.6 seconds. It required
less than 35 Mbytes of memory. We also found that the
runtime overhead to maintain the reference counts is small.
The additional overhead to maintain the reference counts
(when compared to a simple malloc/free interface) varied
between 1.5 % and 7.35 % of the total message processing
cost.

Acknowledgments

This work was supported in part by the National Science
Foundation (CDA-9624099,EIA-9975011,ANI-9906704,EIA-
9975011), the Department of Energy (DE-FC02-99ER25387),
California Institute of Technology (PC-159775, PC-228905),
Sandia National Lab (AO-5098.A06), Lawrence Livermore
Laboratory (B347877), Intel Research Council, and the Intel
Technology 2000 equipment grant.
8.



--R



Using Network Interface Support to Avoid Asynchronous Protocol Processing in Shared Virtual Memory Systems.
A Gigabit-per-Second Local Area Network

Porting a User-Level Communication Architecture to NT: Experiences and Performance
Reducing Sweep Time for a Nearly Empty Heap.
Enforcing High-Level Protocols in Low-Level Software

Design and Implementation of Virtual Memory-Mapped Communication on Myrinet
Static Detection of Dynamic Memory Errors.

Fast Detection of Memory Leaks and Access Errors.
Communicating Sequential Processes.
The Spin Model Checker.
ESP: A Language for Programmable Devices.
ESP: A Language for Programmable Devices.
High Performance Messaging on Workstations: Illinois Fast Messages (FM) for Myrinet.
Implementation of the Typed Call-by-Value lambda-Calculus Using a Stack of Regions

Active Messages: A Mechanism for Integrated Communication and Computation.
Evolution of Virtual Interface Architecture.
A First Step Towards Automated Detection of Bu

Virtual Log Based File Systems for a Programmable Disk.
Uniprocessor Garbage Collection Techniques.
The SPLASH-2 Programs: Characterization and Methodological Considerations
--TR
Active messages
Implementation of the typed call-by-value MYAMPERSAND#955;-calculus using a stack of regions
The SPLASH-2 programs
U-Net
High performance messaging on workstations
Static detection of dynamic memory errors
The Model Checker SPIN
Active disks
Virtual log based file systems for a programmable disk
Using network interface support to avoid asynchronous protocol processing in shared virtual memory systems
Reducing sweep time for a nearly empty heap
Communicating sequential processes
Enforcing high-level protocols in low-level software
Region-based memory management in cyclone
High-Speed Data Paths in Host-Based Routers
User-Level Network Interface Protocols
Evolution of the Virtual Interface Architecture
Myrinet
Design and Implementation of Virtual Memory-Mapped Communication on Myrinet
Uniprocessor Garbage Collection Techniques

--CTR
Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, Proceedings of the 5th symposium on Operating systems design and implementation Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading, December 09-11, 2002, Boston, Massachusetts
Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002
programmable devices;reference counting;dynamic memory management;model checking