436
S. Wimmer and J. von Mutius
2.5 Parallel Execution
The attentive reader may wonder why we care about a purely functional implementation of the certificate checker at all. Indeed, we could use existing techniques
[31] to obtain an imperative implementation of the certificate checker in the
heap monad. However, in this setting it would be hard to justify the soundness
of executing parts of the checker in parallel. In the purely functional setting,
this is much simpler. Our approach to parallel execution is minimalist: we only
provide means to execute the map combinator on lists in parallel. This is achieved
by another custom code translation that is part of the trusted code base. The
parallel implementation of map uses a task queue that will contain the individual
computations that need to be run for each element of xs, and uses a fixed number
of threads to work through this list and assemble the final result.
We exploit this map implementation to work through the list of discrete states
L in parallel, using the equivalence:
list all Q xs = list all id (map Q xs) .
In doing so, we lose the ability to stop execution early once a list element does
not satisify Q. For the certificate checker, however, we assume that usually
the certificate is correct, meaning that we have to go through the whole list
anyway. We only parallelize the outermost loop of check i because this should
yield reasonably-sized work portions, given that the size of L will typically at
least be in the hundreds.
3 Scaling Performance
In this section we discuss two techniques to improve the performance of the
certificate checker without increasing the verification effort significantly.
3.1 Monomorphization
Isabelle/HOL supports polymorphism and type classes, which are valuable features for sizeable formalization efforts. Large parts of our formalization also make
use of these features, e.g., most of the timed automata semantics are formalized
for a general time domain, and operations on DBMs are applicable on DBMs
whose entries are formed from more general algebraic structures than the ring of
integers. While this yields an abstract and general formalized theory, it can get
in our way when trying to obtain efficient code.
When generating SML code from HOL, Isabelle uses a so-called dictionary
construction to compile out type classes, which are not supported by SML. This
means that most functions carry a large number of additional parameters, which
are used to look up elementary operations, such as addition of two numbers.
These additional lookup operations degrade performance. One solution is to
ensure that all relevant constants that are exported to SML are monomorphic
(i.e. specialized to the integer type), eliminating the need for the dictionary
construction in most places. Thus, we apply a semi-automated procedure to
achieve this monomorphization.
S. Wimmer and J. von Mutius
2.5 Parallel Execution
The attentive reader may wonder why we care about a purely functional implementation of the certificate checker at all. Indeed, we could use existing techniques
[31] to obtain an imperative implementation of the certificate checker in the
heap monad. However, in this setting it would be hard to justify the soundness
of executing parts of the checker in parallel. In the purely functional setting,
this is much simpler. Our approach to parallel execution is minimalist: we only
provide means to execute the map combinator on lists in parallel. This is achieved
by another custom code translation that is part of the trusted code base. The
parallel implementation of map uses a task queue that will contain the individual
computations that need to be run for each element of xs, and uses a fixed number
of threads to work through this list and assemble the final result.
We exploit this map implementation to work through the list of discrete states
L in parallel, using the equivalence:
list all Q xs = list all id (map Q xs) .
In doing so, we lose the ability to stop execution early once a list element does
not satisify Q. For the certificate checker, however, we assume that usually
the certificate is correct, meaning that we have to go through the whole list
anyway. We only parallelize the outermost loop of check i because this should
yield reasonably-sized work portions, given that the size of L will typically at
least be in the hundreds.
3 Scaling Performance
In this section we discuss two techniques to improve the performance of the
certificate checker without increasing the verification effort significantly.
3.1 Monomorphization
Isabelle/HOL supports polymorphism and type classes, which are valuable features for sizeable formalization efforts. Large parts of our formalization also make
use of these features, e.g., most of the timed automata semantics are formalized
for a general time domain, and operations on DBMs are applicable on DBMs
whose entries are formed from more general algebraic structures than the ring of
integers. While this yields an abstract and general formalized theory, it can get
in our way when trying to obtain efficient code.
When generating SML code from HOL, Isabelle uses a so-called dictionary
construction to compile out type classes, which are not supported by SML. This
means that most functions carry a large number of additional parameters, which
are used to look up elementary operations, such as addition of two numbers.
These additional lookup operations degrade performance. One solution is to
ensure that all relevant constants that are exported to SML are monomorphic
(i.e. specialized to the integer type), eliminating the need for the dictionary
construction in most places. Thus, we apply a semi-automated procedure to
achieve this monomorphization.