Proving Correctness of a Distributed Shared Memory Implementation
DiSOM [3,4,2] is a distributed shared memory system that offers users an atomic collection of memory cells provided they satisfy certain well-formedness conditions. This report proves the correctness of DiSOM. The system partitions memory into a set of objects and implicitly associates a read-write...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149294 |
| Summary: | DiSOM [3,4,2] is a distributed shared memory system that offers users an atomic collection of memory cells provided they satisfy certain well-formedness conditions. This report proves the correctness of DiSOM. The system partitions memory into a set of objects and implicitly associates a read-write lock with each object. Users synchronize accesses to these objects-write implementation guarantees progress and the usual read-write lock exclusions conditions. |
|---|