Proving Correctness of a Lock-based Cache Coherency Protocol for a Cluster File System
Jin He
Abstract
Jin He
Abstract
Cluster file system is an important component of cluster operating system,and client-side caching is one of the key issues that address the performance problem of cluster file system.However,there is little study on the formalization of file system semantics and verification of cache coherency proto-col in cluster file system.This paper presents a new cache co-herency protocol to achieve UNIX semantics in cluster file sys-tem by extending the capability of POSIX file lock API and gives the formal proof using I/O automata theory.This protocol has been implemented in DCFS(Dawning Cluster File System).
A significance statement is not available in the OpenAlex record.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
Cluster file system is an important component of cluster operating system,and client-side caching is one of the key issues that address the performance problem of cluster file system.However,there is little study on the formalization of file system semantics and verification of cache coherency proto-col in cluster file system.This paper presents a new cache co-herency protocol to achieve UNIX semantics in cluster file sys-tem by extending the capability of POSIX file lock API and gives the formal proof using I/O automata theory.This protocol has been implemented in DCFS(Dawning Cluster File System).
Key concepts: Computer science, Unix file types, Operating system, Virtual file system, Self-certifying File System, Cache, Versioning file system, File system