feat: rename awkernel_async_lib_verified to awkernel_lib_verified (#774)

Author: romancardenas

.cargo/config.toml

@@ -40,7 +40,7 @@ udeps_lib_rv64 = "udeps --package awkernel_lib --no-default-features --features
 udeps_async_lib = "udeps --package awkernel_async_lib --no-default-features --features std"
 udeps_drivers_x86 = "udeps --package awkernel_drivers --no-default-features --features x86"
 udeps_drivers_raspi = "udeps --package awkernel_drivers --no-default-features --features aarch64 --features raspi --features pl011"
-udeps_async_lib_verified = "udeps --package awkernel_async_lib_verified"
+udeps_lib_verified = "udeps --package awkernel_lib_verified"
 
 [target.'cfg(target_os = "linux")']
 rustflags = ["-C", "link-arg=-lc", "-C", "link-arg=-lpthread"]

Cargo.toml

@@ -6,7 +6,7 @@ members = [
     "userland",
     "x86bootdisk",
     "awkernel_async_lib",
-    "awkernel_async_lib_verified",
+    "awkernel_lib_verified",
     "awkernel_lib",
     "awkernel_drivers",
     "applications/awkernel_services",

README.md

@@ -37,8 +37,8 @@ $ cargo binstall mdbook-mermaid
   - library used by both [kernel](./kernel/) and [awkernel_async_lib](./awkernel_async_lib/)
 - [awkernel_async_lib](./awkernel_async_lib/)
   - asynchronous library for no_std
-- [awkernel_async_lib_verified](./awkernel_async_lib_verified/)
-  - verified library for awkernel_async_lib
+- [awkernel_lib_verified](./awkernel_lib_verified/)
+  - shared data structures with Kani proof harnesses, re-exported as `awkernel_lib::verified`
   - pure Rust (no dependencies on external functions and no inline assembly)
 - [awkernel_futures_macro](./awkernel_futures_macro/)
 - [awkernel_macros](./awkernel_macros/)
@@ -50,7 +50,7 @@ $ cargo binstall mdbook-mermaid
 
 ```mermaid
 graph TD;
-    awkernel_async_lib-->awkernel_async_lib_verified;
+    awkernel_lib-->awkernel_lib_verified;
     awkernel_async_lib-->awkernel_futures_macro;
     awkernel_async_lib-->awkernel_lib;
     awkernel_lib-->awkernel_sync;

SPEC_TEST.md

@@ -16,8 +16,8 @@
 | [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+ |
 | [Context Switch of x86_64](./awkernel_lib/src/context/x86_64.rs) | [context/x86](./specification/awkernel_lib/src/context/x86/) | TLA+ |
-| [Delta List](./awkernel_async_lib_verified/src/delta_list.rs) | unit test | Kani |
-| [Ring Queue](./awkernel_async_lib_verified/src/ringq.rs) | unit test | Kani |
+| [Delta List](./awkernel_lib_verified/src/delta_list.rs) | unit test | Kani |
+| [Ring Queue](./awkernel_lib_verified/src/ringq.rs) | unit test | Kani |
 | Sleep CPU (no_std) | [awkernel_async_lib/src/task/wake_workers_no_std](./specification/awkernel_async_lib/src/task/wake_workers_no_std) | SPIN |
 | Sleep CPU (std) | [awkernel_async_lib/src/task/wake_workers](./specification/awkernel_async_lib/src/task/wake_workers) | SPIN |
 | [if_net](./awkernel_lib/src/net/if_net.rs) | [awkernel_lib/src/net/if_net](./specification/awkernel_lib/src/net/if_net) | SPIN |

awkernel_async_lib/Cargo.toml

@@ -28,9 +28,6 @@ features = ["alloc", "async-await", "async-await-macro"]
 path = "../awkernel_lib"
 default-features = false
 
-[dependencies.awkernel_async_lib_verified]
-path = "../awkernel_async_lib_verified"
-
 [dependencies.awkernel_futures_macro]
 path = "../awkernel_futures_macro"
 

awkernel_async_lib/src/channel/bounded.rs

@@ -16,10 +16,10 @@
 
 use crate::{pubsub::Lifespan, r#yield};
 use alloc::sync::Arc;
-use awkernel_async_lib_verified::ringq::RingQ;
 use awkernel_lib::{
     delay::uptime,
     sync::mutex::{MCSNode, Mutex},
+    verified::ringq::RingQ,
 };
 use core::task::{Poll, Waker};
 use futures::Future;

awkernel_async_lib/src/pubsub.rs

@@ -39,10 +39,12 @@ use alloc::{
     sync::Arc,
     vec::Vec,
 };
-use awkernel_async_lib_verified::ringq::RingQ;
-use awkernel_lib::sync::{
-    mutex::{MCSNode, Mutex},
-    rwlock::RwLock,
+use awkernel_lib::{
+    sync::{
+        mutex::{MCSNode, Mutex},
+        rwlock::RwLock,
+    },
+    verified::ringq::RingQ,
 };
 use core::{
     pin::Pin,

awkernel_async_lib/src/scheduler.rs

@@ -10,10 +10,10 @@ use crate::{
 };
 use alloc::collections::{binary_heap::BinaryHeap, btree_map::BTreeMap};
 use alloc::sync::Arc;
-use awkernel_async_lib_verified::delta_list::DeltaList;
 use awkernel_lib::{
     cpu::{num_cpu, CpuSet},
     sync::mutex::{MCSNode, Mutex},
+    verified::delta_list::DeltaList,
 };
 
 #[cfg(not(feature = "std"))]

awkernel_drivers/Cargo.toml

@@ -43,9 +43,6 @@ optional = true
 path = "../awkernel_lib"
 default-features = false
 
-[dependencies.awkernel_async_lib_verified]
-path = "../awkernel_async_lib_verified"
-
 [dependencies.bootloader_api]
 version = "0.11"
 optional = true

awkernel_drivers/src/ic/genet.rs

@@ -1,4 +1,3 @@
-use awkernel_async_lib_verified::ringq::RingQ;
 use awkernel_lib::{
     addr::{virt_addr::VirtAddr, Addr},
     dma_pool::DMAPool,
@@ -12,6 +11,7 @@ use awkernel_lib::{
     },
     paging::PAGESIZE,
     sync::{mcs::MCSNode, mutex::Mutex, rwlock::RwLock},
+    verified::ringq::RingQ,
 };
 
 use alloc::{boxed::Box, sync::Arc, vec::Vec};