Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems

ate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems Ankush Desai1 , Sanjit A. Seshia1 , Shaz Qadeer2 , David Broman1,3 , John C. Eidson1 1 University of California at Berkeley, CA, USA 2 Microsoft Research, Redmond, USA 3 KTH Royal Institute of Technology, Sweden Abstract. Forms of synchrony can greatly simplify modeling, design, and verification of distributed systems. Thus, recent advances in clock synchronization protocols and their adoption hold promise for system design. However, these protocols synchronize the distributed clocks only within a certain tolerance, and there sient phases while synchronization is still being achieved. Abstractions used for modeling and verification of such systems should accurately capture these imperfections that cause the system to only be “almost synchronized.” In er, we present approximate synchrony, a sound and tunable abstraction for verification of almost-synchronous systems. We show how approximate synchrony can be ...

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, John C. Eidson
• Keywords: CAV 2015, Hardware