doc: Improve readme

Signed-off-by: Diogo Behrens <[email protected]>

Author: db7

.github/workflows/actions.yml

@@ -15,6 +15,7 @@ jobs:
       include:   ${{ steps.include.outputs.changed }}
       verify:    ${{ steps.verify.outputs.changed }}
       test:      ${{ steps.test.outputs.changed }}
+      markdown:  ${{ steps.markdown.outputs.changed }}
     steps:
       - uses: dorny/paths-filter@v3
         id: include
@@ -33,14 +34,27 @@ jobs:
         with:
           filters: |
             changed:
-              - 'verify/**'
+              - 'verify/**.bpl'
+      - uses: dorny/paths-filter@v3
+        id: markdown
+        with:
+          filters: |
+            changed:
+              - '**.md'
       - uses: dorny/paths-filter@v3
         id: test
         with:
           filters: |
             changed:
               - 'test/**'
 
+  print-changed:
+    name: Print information about changed paths
+    needs: changed
+    runs-on: ubuntu-latest
+    steps:
+      - run: echo "${{ needs.changed.outputs.markdown }}"
+
   test-install:
     strategy:
       matrix:

README.md

@@ -10,14 +10,73 @@ with a model checker such as [Dartagnan][] or [vsyncer][].
 
 The atomics implementations are being gradually verified to comply with VMM. At
 the moment, we have completed the verification of ARMv8 64-bits with and
-without LSE instructions.
+without LSE instructions, and RISC-V using compiler builtins.
 
 This project is a spinoff of the VSync project and a key component in
-[libvsync][].
-
-Refer to our ASPLOS'21 [publication][paper] describing part of the
+[libvsync][]. Refer to our ASPLOS'21 [publication][paper] describing part of the
 research effort put into this library.
 
+## Getting started
+
+```sh
+cmake -S . -B build
+cmake --build build
+ctest --test-dir build --output-on-failure
+cmake --install build --prefix /desired/prefix
+```
+
+`vatomic` installs headers under `include/vsync/` and a CMake package file,
+allowing downstream projects to simply `find_package(vatomic CONFIG REQUIRED)`
+and link against the `vatomic::vatomic` interface target.
+
+### Using the C API
+
+```c
+#include <vsync/atomic.h>
+
+void example(void)
+{
+    vatomic32_t counter;
+    vatomic32_write_rlx(&counter, 0);
+    vuint32_t old = vatomic32_add(&counter, 2);
+    (void)old;
+}
+```
+
+### Using the C++ API
+
+```c++
+#include <vsync/atomic.hpp>
+
+void example()
+{
+    vsync::atomic<int> counter{};
+    counter.store(42, vsync::memory_order_relaxed);
+    auto prev = counter.fetch_add(1);
+    (void)prev;
+}
+```
+
+## Testing and verification
+
+Besides the unit tests (`ctest`) the repository ships a Boogie-based
+verification harness. To run it locally:
+
+```sh
+cmake -S . -B build -DVATOMIC_DEV=ON
+cmake --build build --target build_boogie_lse
+ctest --test-dir build/verify -R lse --output-on-failure
+```
+
+Targets exist for `lse`, `llsc`, `lxe`, and `no_polite_await`. Refer to
+[`verify/README.md`](verify/README.md) for dependency details.
+
+## Releases and support
+
+Changes between versions are tracked in [CHANGELOG.md](CHANGELOG.md). Issues
+and pull requests are welcome in this repository; please include details about
+the architecture, compiler, and toolchain you are using.
+
 ## Acknowledgements
 
 This project was initially developed under the support of