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

June 5th, 2008

Categories: Applications, Architecture, Networking, Software, Supercomputing

Client-Server Pair Abstraction
Client-Server Pair Abstraction

Authors

Vishwanath, V., Zuck, L., Leigh, J.

About

LambdaRAM is a high-performance, multi-dimensional, 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 Modeling, Analysis and Prediction (MAP) Program applications to study tropical cyclones. Formal verification of 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.

Resources

PDF

URL

Citation

Vishwanath, V., Zuck, L., Leigh, J., Specification and Verification of LambdaRAM - A Wide-Area Distributed Cache for High Performance Computing, Sixth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE ’2008), Anaheim, CA, June 5th, 2008. http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4547672&arnumber=4547709&count=42&index=36