Information Technology Reference
In-Depth Information
a)
b)
0010 ****
0010 ****
00100110
00101 ***
0010011 *
00101 ***
00101001
00101101
00100110 00100111
00101001 00101101
Fig. 5. Example of a Patricia trie a) before, and b) after inserting 00100111
Thanks to these primitives, the (unoptimized) instrumentation for record-
ing in the store is mostly straightforward. To monitor the block of an argu-
ment or a local variable v of type T in function f , e-acsl2c adds the calls
__store_block(&v, sizeof (T)) in the beginning, and __delete_block(&v) at the end of
the scope of v . For a global variable, these calls are inserted in the beginning
and at the end of the function main . In addition to them, for global variables
(initialized by default to 0 in C) and function arguments (initialized by a func-
tion call), the __store_block(&v, sizeof (T)) is followed by __full_init(&v) to mark
the whole block as initialized. To monitor an assignment v = exp; to a variable
(or a left value) v ,acallto __initialize(&v, sizeof (v)); is inserted. Literal strings
and initializers are easily handled as well. Finally, dynamic allocation functions
are simply replaced by their instrumented counterparts.
4 Optimized Storage for the Memory Monitoring Library
Ecient implementation of the store requires a data structure with a good time
and space complexity, since the instrumented code may perform frequent modi-
fications and lookups in the store. It is intuitively clear that the structure has to
be sorted: treating e-acsl constructs may require to access a block metadata di-
rectly by its base address as well as to find a block's predecessor or successor. For
example, the query __base_addr(p) searches the store for the closest to p base ad-
dress less than p (and checks the bounds afterwards). Thus, a hash table will not
fit. Lists are not ecient enough due to a linear worst-case complexity. Unbal-
anced binary search trees have a linear worst-case complexity too when inserted
base addresses are monotonically increasing, and this may be quite common.
Finally, the cost of balancing (e.g. in a self-balancing binary search tree) would
be amortized if the store modifications (that may lead to rebalancing) were less
frequent than simple queries (that take advantage of a balanced structure). For
tested examples of code instrumented by e-acsl2c this is not necessarily true.
Our implementation of the store is based on a Patricia trie [8], also known as
a radix tree or compact prefix tree , which is ecient even if the tree is unbalanced.
Node keys are base addresses (e.g. 32-bit or 64-bit words) or address prefixes.
Any leaf contains a block metadata with the block base address. Routing from
the root to a block metadata is ensured by internal nodes, each of them contains
the greatest common prefix of base addresses stored in its successors.
For instance, Fig. 5a shows a Patricia trie, for simplicity, over 8-bit addresses.
It contains three blocks in its leaves (only block base addresses are shown here),
and greatest common prefixes in internal nodes. A “ * ” denotes meaningless bits
 
Search WWH ::




Custom Search