Skip to content

Commit 8d63881

Browse files
authored
sync dv; update readme (#360)
1 parent f4091dc commit 8d63881

2 files changed

Lines changed: 2 additions & 2 deletions

File tree

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ This work is ongoing. Our current focus is on verifying OSTD’s *memory managem
1212

1313
## Project Structure
1414

15-
Implementation code from the OSTD [mainline](https://github.com/asterinas/asterinas), together with its accompanying proofs, resides in the `aster_common` and `ostd` directories, while specifications are located under `specs`.
15+
Implementation code from the OSTD [mainline](https://github.com/asterinas/asterinas), together with its accompanying proofs, resides in the `ostd` directory, while specifications are located under `specs`.
1616

1717
This repository currently contains verification code for `ostd/src/mm` and `ostd/src/sync`. It is independent of the concurrency proofs presented in our [SOSP paper](https://dl.acm.org/doi/10.1145/3731569.3764836)*“CortenMM: Efficient Memory Management with Strong Correctness Guarantees.”* For the SOSP artifact, please refer to the [func-correct](https://github.com/asterinas/vostd/tree/func-correct) branch for verification code, and to [this repo](https://github.com/TELOS-syslab/CortenMM-Artifact) for the complete artifact.
1818

dv

0 commit comments

Comments
 (0)