vix.ing · top · new · best · stats · spec

CausalMesh: A Formally Verified Causal Cache for Stateful Serverless Computing

2025/08/21 by Zhang, Haoran, Zhang, Zihao, Mu, Shuai +2
#Distributed #FOS: Computer and information sciences #Parallel #and Cluster Computing (cs.DC)

paper · doi:10.48550/arxiv.2508.15647

Abstract

Stateful serverless workflows consist of multiple serverless functions that access state on a remote database. Developers sometimes add a cache layer between the serverless runtime and the database to improve I/O latency. However, in a serverless environment, functions in the same workflow may be scheduled to different nodes with different caches, which can cause non-intuitive anomalies. This paper presents CausalMesh, a novel approach to causally consistent caching in environments where a computation may migrate from one machine to another, such as in serverless computing. CausalMesh is the first cache system that supports coordination-free and abort-free read/write operations and read transactions when clients roam among multiple servers. CausalMesh also supports read-write transactional causal consistency in the presence of client roaming, but at the cost of abort-freedom. We have formally verified CausalMesh's protocol in Dafny, and our experimental evaluation shows that CausalMesh has lower latency and higher throughput than existing proposals

Citations

Related