Verifying Concurrency in an Adaptive Ocean Circulation
Model
Author/Presenters
Event Type
Workshop
Applications
Correctness
Debugging
Reliability
SIGHPC Workshop
Verification
TimeSunday, November 12th10:30am -
10:47am
Location501
DescriptionWe present a model checking approach for verifying the
correctness of concurrency in numerical models. The
forms of concurrency we address are from (1) coupled
modeling where distinct components, e.g., ocean, wave,
and atmospheric, exchange interface conditions during
runtime, and (2) multi-instance modeling where local
variations of the same numerical model are executed
concurrently to minimize common (and therefore
redundant) computations. We present general guidelines
for representing these forms of concurrency in an
abstract verification model and then apply them to an
adaptive ocean circulation model that determines the
geographic extent and severity of coastal floods. The
ocean model employs multi-instance concurrency: a
collection of engineering design and failure scenarios
are concurrently simulated using patches, regions of a
grid that grow and shrink based on the hydrodynamic
changes induced by each scenario. We show how
concurrency inherent in the simulation model can be
represented in a verification model to ensure
correctness and to automatically generate safe
synchronization arrangements.
