Specification and Verification of LambdaRAM- A Wide-area Distributed Cache for High Performance Computing

LambdaRAM is a high-performance, multidimensional, wide-area, distributed cache that takes advantage of massively available memory from multiple clusters interconnected by ultra high-speed networking to provide data-intensive scientific applications with rapid access to both local and remote data without suffering the latency bottlenecks often associated with large storage systems and wide-area data access. LambdaRAM has been demonstrated to yield significant performance speed-ups for geophysical and Bioscience applications accessing extremely large datasets. Currently, LambdaRAM is being integrated by NASA for the modelling, analysis and prediction (MAP) program applications to study tropical cyclones. Formal verification o/LambdaRAM is important to NASA to ensure that LambdaRAM operates reliably in real-time mission critical deployments. We present our preliminary steps towards full formal verification of LambdaRAM. We first give an abstract description of the system and then verify several of its properties. Most of the proofs are accomplished by automatic techniques, while some require deductive steps.