Abstract
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.37 % of the total message processing cost (in the worst case) over a malloc/free interface.
Original language | English (US) |
---|---|
Pages | 139-149 |
Number of pages | 11 |
DOIs | |
State | Published - 2002 |
Event | ISMM 2002: The 2002 International Symposium on Memory Management - Berlin, Germany Duration: Jun 20 2002 → Jun 21 2002 |
Other
Other | ISMM 2002: The 2002 International Symposium on Memory Management |
---|---|
Country/Territory | Germany |
City | Berlin |
Period | 6/20/02 → 6/21/02 |
All Science Journal Classification (ASJC) codes
- Computer Science (miscellaneous)
Keywords
- Dynamic memory management
- Model checking
- Programmable devices
- Reference counting