From 7b21be4169cdbb555778620751d77817d87c12ff Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 26 Aug 2025 15:13:10 +0900 Subject: [PATCH 1/2] fix(README): update README.md Signed-off-by: Yuuki Takano --- README.md | 131 ++++++++---------------------------------------------- 1 file changed, 18 insertions(+), 113 deletions(-) diff --git a/README.md b/README.md index 33689a658..5a7530a06 100644 --- a/README.md +++ b/README.md @@ -3,83 +3,6 @@ Awkernel is a safe and realtime operating system. It can execute async/await applications in kernel space safely. -## Progress - -- [x] Zero-copy communications - - [x] Publish and subscribe - - [x] Service - - [x] Action -- [x] Channels - - [x] Bounded channel - - [x] Unbounded channel - - [x] Session-type based channel -- [x] Memory space isolation -- [x] Timer interrupts - - [x] AArch64 - - [x] x86_64 -- [x] Interrupt Controllers - - [x] AArch64 - - [x] Raspberry Pi 3 - - [x] GICv2 - - [x] GICv3 - - [x] x86_64 - - [x] xAPIC - - [x] x2APIC -- [ ] Frame buffer - - [ ] AArch64 virt - - [x] Raspberry Pi 3 and 4 - - [x] x86_64 -- [ ] Diagnostics -- [ ] Measurement -- [ ] Power Management - - [ ] Shutdown - - [ ] Reboot -- [ ] Schedulers - - [x] Prioritized FIFO scheduler - - [ ] Prioritized Round robin scheduler - - [ ] EDF scheduler - - [ ] DAG scheduler -- [ ] Memory allocators - - [x] O(1) memory allocator - - [x] DMA pool - - [ ] NUMA aware memory allocator -- [ ] DVFS - - [ ] AArch64 - - [ ] x86_64 -- [ ] PCIe - - [ ] MSI - - [x] x86_64 xAPIC and x2APIC - - [ ] AArch64 GICv3 - - [ ] MSI-X - - [x] x86_64 xAPIC and x2APIC - - [ ] AArch64 GICv3 -- Network controllers - - [x] Intel Gb Ethernet Controller (e1000 Series) - - [ ] Intel 2.5Gb Ethernet Controller (I225/I226 series) - - [x] Intel 10Gb Ethernet Controller (X520 Series) - - [ ] Mellanox ConnectX-5 series - - [x] genet for Raspberry Pi -- Networking - - [x] IPv4 - - [ ] IPv6 - - [x] UDP - - [x] TCP - - [ ] VLAN - - [x] IP multicast - - [ ] Offloading - - [ ] TSO - - [ ] IPv4 header checksum - - [x] UDP checksum - - [ ] TCP checksum - - [ ] VLAN hardware tagging -- [ ] XHCI -- [ ] Block devices - - [ ] NVMe - - [ ] AHCI -- [ ] File systems - - [ ] FAT32 - - [ ] Journaling file system - ## Dependencies ### Compiler Tools @@ -185,16 +108,16 @@ etc ### Compile -Debug build. +Release build (recommended). ```text -$ make x86_64 +$ make x86_64 RELEASE=1 ``` -Release build. +Debug build. ```text -$ make x86_64 RELEASE=1 +$ make x86_64 ``` ### Boot @@ -216,16 +139,16 @@ $ make gdb-x86_64 ### Compile -Debug build. +Release build (recommended). ```text -$ make aarch64 BSP=aarch64_virt +$ make aarch64 BSP=aarch64_virt RELEASE=1 ``` -Release build. +Debug build. ```text -$ make aarch64 BSP=aarch64_virt RELEASE=1 +$ make aarch64 BSP=aarch64_virt ``` ### Boot @@ -247,7 +170,7 @@ $ make gdb-aarch64_virt ### Compile -Release build. +Release build (recommended). `RELEASE=1` must be used for actual devices. ```text @@ -294,40 +217,22 @@ $ make aarch64 BSP=raspi4 RELEASE=1 --- -## Raspberry Pi 5 (AArch64) +## RISC-V (64bit, Qemu) ### Compile -Specify `Release=1`. +Release build (recommended). ```text -$ make aarch64 BSP=raspi5 RELEASE=1 +$ make riscv64 RELEASE=1 ``` -### Boot - -- Serial - - 8N1: eight data bits, no parity, one stop bit - - Speed: 115200 - ---- - -## RISC-V (64bit, Qemu) - -### Compile - Debug build. ```text $ make riscv64 ``` -Release build. - -```text -$ make riscv64 RELEASE=1 -``` - ### Boot ```text @@ -340,16 +245,16 @@ $ make qemu-riscv64 ### Compile -Debug build. +Release build (recommended). ```text -$ make riscv32 +$ make riscv32 RELEASE=1 ``` -Release build. +Debug build. ```text -$ make riscv32 RELEASE=1 +$ make riscv32 ``` ### Boot @@ -419,6 +324,6 @@ $ make loom [Publications](./PUBLICATIONS.md) -## Verification +## Specification by Formal Methods -[Verification Result](./VERIFICATION.md) +[Specification](./specification) From e97440bc580ca4f4877cd5fc7fe0b834e3df771b Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 26 Aug 2025 15:17:13 +0900 Subject: [PATCH 2/2] move VERIFICATION.md SPEC_TEST.md Signed-off-by: Yuuki Takano --- README.md | 7 +++++-- VERIFICATION.md => SPEC_TEST.md | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) rename VERIFICATION.md => SPEC_TEST.md (97%) diff --git a/README.md b/README.md index 5a7530a06..7bde87be4 100644 --- a/README.md +++ b/README.md @@ -122,6 +122,9 @@ $ make x86_64 ### Boot +Qemu 8.x or later is required. +Qemu 6.x is not supported. + ```text $ make qemu-x86_64 ``` @@ -324,6 +327,6 @@ $ make loom [Publications](./PUBLICATIONS.md) -## Specification by Formal Methods +## Specification and Test Results -[Specification](./specification) +[Specification and Test Results](./SPEC_TEST.md) diff --git a/VERIFICATION.md b/SPEC_TEST.md similarity index 97% rename from VERIFICATION.md rename to SPEC_TEST.md index 50d76fe66..78afaf43b 100644 --- a/VERIFICATION.md +++ b/SPEC_TEST.md @@ -1,4 +1,4 @@ -# Verification Result +# Specification and Test Results ## Tools