add atomic sanity test

Author: fhackett

omnilink/atomic/Atomic.tla

@@ -0,0 +1,16 @@
+---- MODULE Atomic ----
+EXTENDS Integers
+
+VARIABLE x
+
+Inc(prev_x) ==
+    /\ prev_x = x
+    /\ x' = x + 1
+
+Init ==
+    x = 1
+
+Next ==
+    Inc(x)
+
+====

omnilink/atomic/MCAtomic.cfg

@@ -0,0 +1,3 @@
+INIT Init
+NEXT Next
+CONSTRAINT StateConstraint

omnilink/atomic/MCAtomic.tla

@@ -0,0 +1,7 @@
+---- MODULE MCAtomic ----
+EXTENDS Atomic
+
+StateConstraint ==
+    x <= 5
+
+====

omnilink/atomic/MCAtomicValidate.cfg

@@ -0,0 +1,6 @@
+INIT Init
+NEXT Next
+
+ALIAS DebugAlias
+POSTCONDITION PostCondition
+CHECK_DEADLOCK FALSE

omnilink/atomic/MCAtomicValidate.tla

@@ -0,0 +1,7 @@
+---- MODULE MCAtomicValidate ----
+EXTENDS AtomicValidate
+
+DebugAlias == __TraceOps!DebugAlias
+PostCondition == __TraceOps!PostCondition
+
+====

omnilink/atomic/package.mill

@@ -0,0 +1,25 @@
+package build.omnilink.atomic
+
+import mill.*
+
+def theSpec = Task.Source(os.sub / "Atomic.tla")
+def theSpecToValidateMC =
+  Task.Source(os.sub / "MCAtomicValidate.tla")
+def theSpecToValidateMCConfig =
+  Task.Source(os.sub / "MCAtomicValidate.cfg")
+
+object workload extends build.omnilink.TracingConfigModule:
+  def specToValidate = theSpec
+  def specToValidateMC = theSpecToValidateMC
+  def specToValidateMCConfig = theSpecToValidateMCConfig
+  def tracingExecutable = Task:
+    build.omnilink.buildPkg(
+      name = "omnilink.atomic.workload",
+      outPath = os.sub / "bin" / "main",
+    )()
+
+  object defaultConfig extends ConfigModule:
+    def threadCount = 5
+    def operationCount = 10000
+  end defaultConfig
+end workload

omnilink/atomic/workload.nix

@@ -0,0 +1,24 @@
+{
+  stdenv,
+  cmake,
+  omnilink,
+  omnilink_models,
+  msgpack-cxx,
+}:
+stdenv.mkDerivation {
+  pname = "atomic-workload";
+  version = "0.1.0";
+  src = ./workload;
+  dontStrip = true;
+  buildInputs = [
+    omnilink.lib
+    msgpack-cxx
+    omnilink_models.Atomic
+  ];
+  nativeBuildInputs = [
+    cmake
+  ];
+  postInstall = ''
+    chmod a+x $out/bin/main
+  '';
+}

omnilink/atomic/workload/CMakeLists.txt

@@ -0,0 +1,24 @@
+cmake_minimum_required(VERSION 4.1.1)
+project(atomic-stressor)
+
+set(CMAKE_BUILD_TYPE Debug)
+
+# Generate the `compile_commands.json` file.
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON CACHE INTERNAL "")
+
+if(CMAKE_EXPORT_COMPILE_COMMANDS)
+  set(CMAKE_CXX_STANDARD_INCLUDE_DIRECTORIES
+    ${CMAKE_CXX_IMPLICIT_INCLUDE_DIRECTORIES})
+endif()
+
+find_package(msgpack-cxx REQUIRED)
+find_package(OmniLink REQUIRED)
+
+add_executable(main main.cpp)
+target_link_libraries(main msgpack-cxx OmniLink::OmniLink)
+set_property(TARGET main PROPERTY CXX_STANDARD 20)
+set_property(TARGET main PROPERTY CXX_STANDARD_REQUIRED TRUE)
+
+install(DIRECTORY ${PROJECT_BINARY_DIR}/main
+  DESTINATION bin
+)

omnilink/atomic/workload/main.cpp

@@ -0,0 +1,18 @@
+#include <cstdint>
+#include <atomic>
+#include <omnilink/workload.hpp>
+#include <omnilink/models/Atomic.hpp>
+
+struct AtomicWorkloadContext: public omnilink::WorkloadContext<AtomicWorkloadContext, Atomic::AnyOperation> {
+    std::atomic<int32_t> x{1};
+
+    struct RunnerDefns: public WorkloadContext::RunnerDefnsBase<RunnerDefns> {
+        void perform_operation(Ctx<Atomic::Inc>& ctx) {
+            ctx.op.prev_x = workload_context.x.fetch_add(1, std::memory_order_acq_rel);
+        }
+    };
+};
+
+int main() {
+    return AtomicWorkloadContext::main();
+}

omnilink/concurrentqueue/package.mill

@@ -26,6 +26,10 @@ object `package` extends Module:
       )()
     end tracingExecutable
 
+    object thinConfig extends ConfigModule:
+      def threadCount: Int = 2
+      def operationCount: Int = 100000
+    end thinConfig
     object defaultConfig extends ConfigModule:
       def threadCount = 5
       def operationCount = 100