tier4 · ytakano · Dec 24, 2024 · Dec 24, 2024
diff --git a/.cargo/config.toml b/.cargo/config.toml
@@ -5,7 +5,6 @@ rv32 = "build --package awkernel --no-default-features --features rv32 --target
 rv64 = "build --package awkernel --no-default-features --features rv64 --target riscv64gc-unknown-none-elf -Zbuild-std=core,alloc,compiler_builtins -Zbuild-std-features=compiler-builtins-mem"
 std = "build --package awkernel --no-default-features --features std"
 
-test_awkernel_sync = "test --package awkernel_sync --no-default-features --features std"
 test_awkernel_lib = "test --package awkernel_lib --no-default-features --features std"
 test_awkernel_async_lib = "test --package awkernel_async_lib --no-default-features --features std"
 test_awkernel_drivers = "test --package awkernel_drivers --no-default-features --features std"

diff --git a/Cargo.toml b/Cargo.toml
@@ -13,7 +13,6 @@ members = [
     "applications/awkernel_services",
     "applications/awkernel_shell",
     "applications/tests/*",
-    "awkernel_sync",
 ]
 
 resolver = "2"
diff --git a/Makefile b/Makefile
@@ -220,10 +220,6 @@ test: FORCE
 	cargo test_awkernel_async_lib -- --nocapture
 	cargo test_awkernel_drivers
 
-loom: FORCE
-	RUST_BACKTRACE=1 RUSTFLAGS="--cfg loom" cargo +$(RUSTV) test_awkernel_sync --test model_check_mcslock --release -- --nocapture
-	RUST_BACKTRACE=1 RUSTFLAGS="--cfg loom" cargo +$(RUSTV) test_awkernel_sync --test model_check_rwlock --release -- --nocapture
-
 # Format
 
 fmt: FORCE

diff --git a/VERIFICATION.md b/VERIFICATION.md
@@ -10,8 +10,8 @@
 
 | Target | Verification Code | Tool |
 |--------|--------|-----|
-| [MCS Lock](./awkernel_sync/src/mcs.rs) | [model_check_mcslock.rs](./awkernel_lib/tests/model_check_mcslock.rs) | loom |
-| [RW Lock](./awkernel_sync/src/rwlock.rs) | [model_check_rwlock.rs](./awkernel_lib/tests/model_check_rwlock.rs) | loom |
+| [MCS Lock](https://github.com/tier4/awkernel_sync/blob/main/src/mcs.rs) | [model_check_mcslock.rs](https://github.com/tier4/awkernel_sync/blob/main/tests/model_check_mcslock.rs) | loom |
+| [RW Lock](https://github.com/tier4/awkernel_sync/blob/main/src/rwlock.rs) | [model_check_rwlock.rs](https://github.com/tier4/awkernel_sync/blob/main/tests/model_check_rwlock.rs) | loom |
 | [Cooperative Async/await Scheduler](./awkernel_async_lib/src/task.rs) | [cooperative](./specification/awkernel_async_lib/src/task/cooperative/) | TLA+ |
 | [Exception Handler of AArch64](./kernel/asm/aarch64/exception.S) | [exception.S](./specification/kernel/asm/aarch64/exception.S/) | TLA+ |
 | [Context Switch of AArch64](./awkernel_lib/src/context/aarch64.rs) | [context/aarch64](./specification/awkernel_lib/src/context/aarch64/) | TLA+ |

diff --git a/awkernel_lib/Cargo.toml b/awkernel_lib/Cargo.toml
@@ -14,7 +14,7 @@ embedded-graphics-core = "0.4"
 embedded-graphics = "0.8"
 
 [dependencies.awkernel_sync]
-path = "../awkernel_sync"
+git = "https://github.com/tier4/awkernel_sync.git"
 
 [dependencies.awkernel_async_lib_verified]
 path = "../awkernel_async_lib_verified"

diff --git a/awkernel_sync/Cargo.toml b/awkernel_sync/Cargo.toml
diff --git a/awkernel_sync/build.rs b/awkernel_sync/build.rs
diff --git a/awkernel_sync/src/interrupt_guard.rs b/awkernel_sync/src/interrupt_guard.rs
diff --git a/awkernel_sync/src/interrupt_guard/aarch64.rs b/awkernel_sync/src/interrupt_guard/aarch64.rs
diff --git a/awkernel_sync/src/interrupt_guard/rv32.rs b/awkernel_sync/src/interrupt_guard/rv32.rs
diff --git a/awkernel_sync/src/interrupt_guard/rv64.rs b/awkernel_sync/src/interrupt_guard/rv64.rs
diff --git a/awkernel_sync/src/interrupt_guard/std_common.rs b/awkernel_sync/src/interrupt_guard/std_common.rs
diff --git a/awkernel_sync/src/interrupt_guard/x86_64.rs b/awkernel_sync/src/interrupt_guard/x86_64.rs
diff --git a/awkernel_sync/src/lib.rs b/awkernel_sync/src/lib.rs