Build original Ada port core, V client, and x86-64 boot milestone
This commit is contained in:
Admin committed
1 parent
9af96aa1e1
commit
fc2bee6f32
28 files changed
+865
-7
No files matched your search
@@ -15,3 +15,5 @@
|
|||||||
.idea/
|
.idea/
|
||||||
.DS_Store
|
.DS_Store
|
||||||
Thumbs.db
|
Thumbs.db
|
||||||
|
|
||||||
|
*.bexch
|
||||||
@@ -0,0 +1,31 @@
|
|||||||
|
# Contributing to Open Agila
|
||||||
|
|
||||||
|
Start with a small change you can explain and test. A University certificate records completed checks; a contribution also needs working source and evidence.
|
||||||
|
|
||||||
|
## Your first patch
|
||||||
|
|
||||||
|
1. Clone this repository, record `git rev-parse HEAD`, and run `make test` on the supported build environment.
|
||||||
|
2. Choose one issue with a bounded acceptance test. Read the relevant implementation and its public contract before editing.
|
||||||
|
3. Create a branch: `git switch -c my-port-test`.
|
||||||
|
4. Make one focused change. For a bug fix, demonstrate the failure before the fix and success afterward.
|
||||||
|
5. Run the relevant tests; include `make boot-test` when changing shared port or boot code. Never run a development kernel on the production Forge or University machine itself.
|
||||||
|
6. Review `git diff`. Commit source and documentation, not binaries, build output, credentials, or private Agila code.
|
||||||
|
7. Push to your own repository or authorized branch and open a pull request with the problem, behavior, commands, results, and limitations.
|
||||||
|
|
||||||
|
Public reading and cloning do not need an account. Authenticated contributions currently require a Forge account provisioned by the project owner. Lesson progression and certificates do not depend on receiving a human review.
|
||||||
|
|
||||||
|
## Patch evidence template
|
||||||
|
|
||||||
|
- Requirement and affected files:
|
||||||
|
- Before/after behavior:
|
||||||
|
- Exact source revision, toolchain version, and target:
|
||||||
|
- Reproduction/test commands:
|
||||||
|
- Observed results, including one failure or boundary case:
|
||||||
|
- Remaining limitations:
|
||||||
|
- AI assistance used and what you independently checked:
|
||||||
|
|
||||||
|
AI can help draft code or tests, but the contributor must understand the patch, verify referenced APIs, test its behavior, and explain its assumptions. Do not claim tests were run on hardware you did not use.
|
||||||
|
|
||||||
|
**Tagalog:** Unawain ang kontrata at source. Gumawa ng maliit na pagbabago at test na may malinaw na inaasahang resulta. Itala ang aktuwal na resulta at limitasyon. Huwag maglagay ng password o pribadong code sa commit.
|
||||||
|
|
||||||
|
**Bisaya:** Sabta ang kontrata ug source. Paghimo og gamay nga kausaban ug test nga adunay klarong gipaabot nga resulta. Itala ang aktuwal nga resulta ug limitasyon. Ayaw pag-apil og password o pribadong code sa commit.
|
||||||
@@ -26,3 +26,41 @@ help:
|
|||||||
@echo "make run Build and run the host prototype"
|
@echo "make run Build and run the host prototype"
|
||||||
@echo "make clean Remove build output"
|
@echo "make clean Remove build output"
|
||||||
@echo "make rebuild Clean and rebuild"
|
@echo "make rebuild Clean and rebuild"
|
||||||
|
@echo "make test Ada port, C ABI, and V client checks"
|
||||||
|
@echo "make boot-test Build ISO and verify x86-64 QEMU boot"
|
||||||
|
|
||||||
|
V ?= v
|
||||||
|
CC ?= cc
|
||||||
|
|
||||||
|
.PHONY: test host-library v-demo
|
||||||
|
|
||||||
|
host-library:
|
||||||
|
$(GPRBUILD) -p -P host_library.gpr
|
||||||
|
|
||||||
|
v-demo: host-library
|
||||||
|
mkdir -p $(BIN) $(BUILD)/vmodules $(BUILD)/vtmp
|
||||||
|
VMODULES="$(CURDIR)/$(BUILD)/vmodules" VTMP="$(CURDIR)/$(BUILD)/vtmp" $(V) -cc gcc -gc none -o $(BIN)/agila_port_client examples/v_port_client/main.v
|
||||||
|
|
||||||
|
$(BIN)/abi_test: tests/abi_test.c include/agila_ports.h host-library
|
||||||
|
$(CC) -std=c17 -Wall -Wextra -Werror -Iinclude tests/abi_test.c -Lbuild/lib -lagila_host -o $@
|
||||||
|
|
||||||
|
test: all host-library v-demo $(BIN)/abi_test
|
||||||
|
$(GPRBUILD) -p -P ports.gpr
|
||||||
|
$(BIN)/ports_test
|
||||||
|
LD_LIBRARY_PATH="$(CURDIR)/build/lib:$${LD_LIBRARY_PATH:-}" $(BIN)/abi_test
|
||||||
|
LD_LIBRARY_PATH="$(CURDIR)/build/lib:$${LD_LIBRARY_PATH:-}" $(BIN)/agila_port_client
|
||||||
|
|
||||||
|
BOOT_FLAGS := -O2 -fno-pie -fno-stack-protector -mno-red-zone -mgeneral-regs-only -fno-asynchronous-unwind-tables
|
||||||
|
.PHONY: boot boot-test
|
||||||
|
boot:
|
||||||
|
mkdir -p build/boot build/iso/boot/grub
|
||||||
|
gcc $(BOOT_FLAGS) -c boot/start.S -o build/boot/start.o
|
||||||
|
gcc $(BOOT_FLAGS) -ffreestanding -fno-builtin -c boot/memory.c -o build/boot/memory.o
|
||||||
|
gnatmake -c -D build/boot -Icore -gnat2022 -gnatp $(BOOT_FLAGS) boot/boot_main.adb
|
||||||
|
ld -nostdlib -z max-page-size=0x1000 -T boot/linker.ld -o build/open-agila.elf build/boot/start.o build/boot/boot_main.o build/boot/agila_ports.o build/boot/memory.o
|
||||||
|
grub-file --is-x86-multiboot build/open-agila.elf
|
||||||
|
cp build/open-agila.elf build/iso/boot/
|
||||||
|
cp boot/grub.cfg build/iso/boot/grub/grub.cfg
|
||||||
|
grub-mkrescue -d /usr/lib/grub/i386-pc -o build/open-agila.iso build/iso
|
||||||
|
boot-test: boot
|
||||||
|
python3 scripts/boot-smoke.py
|
||||||
@@ -0,0 +1,59 @@
|
|||||||
|
# Open Agila
|
||||||
|
|
||||||
|
Open Agila is an operating-system project in Ada and V. This repository now has a tested host message-port core, an Ada-to-V demonstration, and a minimal x86-64 QEMU boot milestone. It is an early system-building project, with the source and learning path available for contributors.
|
||||||
|
|
||||||
|
The design draws on OpenStep's separation of application frameworks from the OS and MINIX's separation of kernel mechanisms from user services. The owner's specific Open Amiga repository is still awaiting identification; no Amiga code or compatibility layer has been imported. These are design references, not claims of OpenStep, MINIX, or Amiga binary compatibility.
|
||||||
|
|
||||||
|
## What runs
|
||||||
|
|
||||||
|
| Target | Implemented behavior | Boundary |
|
||||||
|
| --- | --- | --- |
|
||||||
|
| `make run` | Original Ada host scaffold with truthful subsystem status | CPU, memory, interrupt, timer, and scheduler initializers remain placeholders |
|
||||||
|
| `make test` | Ada bounded FIFO ports, sender policy, revocation, generation-checked handles; C ABI checks; V client | Single process, single thread, trusted caller IDs; no kernel-enforced isolation |
|
||||||
|
| `make boot-test` | GRUB loads original x86-64 startup; Ada runs the same port core, prints serial proof, and exits QEMU | BIOS/TCG test target; one address space; no scheduler, user services, persistent storage, networking, or desktop |
|
||||||
|
|
||||||
|
The application-facing Flying V SDK remains a separate public project. This V client uses standard V and does not claim to be a Flying V compiler or the private Agila runtime.
|
||||||
|
|
||||||
|
## Reproduce on Ubuntu 24.04 x86-64
|
||||||
|
|
||||||
|
Install official distribution packages in a development machine or VM:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
sudo apt-get update
|
||||||
|
sudo apt-get install make gcc gnat gprbuild python3 qemu-system-x86 grub-pc-bin grub-common xorriso
|
||||||
|
```
|
||||||
|
|
||||||
|
Install V from its official source and record the commit/version. The first milestone was tested using V 0.5.2, commit `7647ce1`. A prebuilt, unexplained executable is not a source dependency.
|
||||||
|
|
||||||
|
```sh
|
||||||
|
git clone https://git.agilaos.com/matt/open_kernel.git
|
||||||
|
cd open_kernel
|
||||||
|
make test V=/absolute/path/to/v
|
||||||
|
make boot-test
|
||||||
|
```
|
||||||
|
|
||||||
|
Expected proof includes:
|
||||||
|
|
||||||
|
```text
|
||||||
|
ADA_PORTS_OK: ...
|
||||||
|
ADA_V_PORTS_OK value=42
|
||||||
|
OPEN_AGILA_X86_64_ADA
|
||||||
|
ADA_PORTS_BOOT_TESTS_OK
|
||||||
|
AGILA_BOOT_OK
|
||||||
|
QEMU_BOOT_SMOKE_PASS
|
||||||
|
```
|
||||||
|
|
||||||
|
The ISO is `build/open-agila.iso`. The smoke test runs for at most 30 seconds, attaches no writable host disk, disables networking, and checks both serial markers and the QEMU exit status. Use it in QEMU; this release has not been validated on physical hardware, UEFI, Arm64, or RISC-V. A terminal banner alone is not evidence that a complete operating system exists.
|
||||||
|
|
||||||
|
## Start contributing
|
||||||
|
|
||||||
|
Read [the architecture](docs/ARCHITECTURE.md), [the ABI contract](docs/HOST_ABI.md), [the roadmap](docs/ROADMAP.md), and [the contribution guide](CONTRIBUTING.md). The [issue tracker](https://git.agilaos.com/matt/open_kernel/issues) contains bounded tasks with acceptance criteria. [Agila University](https://edu.agilaos.com/) provides English, Tagalog, and Bisaya lessons connected to this source.
|
||||||
|
|
||||||
|
- **Tagalog:** I-build ang eksaktong commit, hulaan ang resulta, patakbuhin ang test, at ipaliwanag ang pagbabago. Maliliit at nasusubukang patch ang simula ng kontribusyon.
|
||||||
|
- **Bisaya:** I-build ang eksaktong commit, tag-ana ang resulta, padagana ang test, ug ipasabot ang kausaban. Sugdi sa gagmay ug masulayan nga patch.
|
||||||
|
|
||||||
|
## Source and license
|
||||||
|
|
||||||
|
The existing Agila Open License v1.0 is preserved. This milestone adds original `core/`, `abi/`, `include/`, `tests/`, `examples/v_port_client/`, `boot/`, and build/documentation support. It corrects the host scaffold's output so placeholder initializers are no longer presented as implemented hardware subsystems. It imports no third-party OS code and no private Agila implementation.
|
||||||
|
|
||||||
|
GRUB, QEMU, GNAT, GCC, and V are development dependencies under their respective upstream licenses. The locally generated ISO contains GRUB boot components as well as this kernel; distribution of a combined ISO must retain the applicable upstream notices and source obligations. The Forge milestone publishes source and test evidence; users can reproduce the ISO with the commands above.
|
||||||
@@ -0,0 +1,44 @@
|
|||||||
|
with Agila_Ports;
|
||||||
|
package body Agila_ABI is
|
||||||
|
State : Agila_Ports.Manager;
|
||||||
|
function Create (Owner : Word) return Word is
|
||||||
|
Handle : Word;
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
Agila_Ports.Create (State, Owner, Handle, Result);
|
||||||
|
return Handle;
|
||||||
|
end Create;
|
||||||
|
function Allow_Sender (Handle, Owner, Sender : Word) return Code is
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
Agila_Ports.Allow_Sender (State, Handle, Owner, Sender, Result);
|
||||||
|
return Agila_Ports.Status'Pos (Result);
|
||||||
|
end Allow_Sender;
|
||||||
|
function Revoke_Sender (Handle, Owner, Sender : Word) return Code is
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
Agila_Ports.Revoke_Sender (State, Handle, Owner, Sender, Result);
|
||||||
|
return Agila_Ports.Status'Pos (Result);
|
||||||
|
end Revoke_Sender;
|
||||||
|
function Send (Handle, Caller, Value : Word) return Code is
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
Agila_Ports.Send (State, Handle, Caller, Value, Result);
|
||||||
|
return Agila_Ports.Status'Pos (Result);
|
||||||
|
end Send;
|
||||||
|
function Receive (Handle, Caller : Word; Value : access Word) return Code is
|
||||||
|
Item : Agila_Ports.Message;
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
if Value = null then return Agila_Ports.Status'Pos (Agila_Ports.Invalid_Argument); end if;
|
||||||
|
Agila_Ports.Receive (State, Handle, Caller, Item, Result);
|
||||||
|
Value.all := Item.Value;
|
||||||
|
return Agila_Ports.Status'Pos (Result);
|
||||||
|
end Receive;
|
||||||
|
function Close (Handle, Caller : Word) return Code is
|
||||||
|
Result : Agila_Ports.Status;
|
||||||
|
begin
|
||||||
|
Agila_Ports.Close (State, Handle, Caller, Result);
|
||||||
|
return Agila_Ports.Status'Pos (Result);
|
||||||
|
end Close;
|
||||||
|
end Agila_ABI;
|
||||||
@@ -0,0 +1,18 @@
|
|||||||
|
with Interfaces;
|
||||||
|
with Interfaces.C;
|
||||||
|
package Agila_ABI is
|
||||||
|
subtype Word is Interfaces.Unsigned_32;
|
||||||
|
subtype Code is Interfaces.C.int;
|
||||||
|
function Create (Owner : Word) return Word
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_create";
|
||||||
|
function Allow_Sender (Handle, Owner, Sender : Word) return Code
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_allow_sender";
|
||||||
|
function Revoke_Sender (Handle, Owner, Sender : Word) return Code
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_revoke_sender";
|
||||||
|
function Send (Handle, Caller, Value : Word) return Code
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_send";
|
||||||
|
function Receive (Handle, Caller : Word; Value : access Word) return Code
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_receive";
|
||||||
|
function Close (Handle, Caller : Word) return Code
|
||||||
|
with Export, Convention => C, External_Name => "agila_port_close";
|
||||||
|
end Agila_ABI;
|
||||||
@@ -0,0 +1,69 @@
|
|||||||
|
with Interfaces; use Interfaces;
|
||||||
|
with System.Machine_Code; use System.Machine_Code;
|
||||||
|
with Agila_Ports; use Agila_Ports;
|
||||||
|
procedure Boot_Main (Magic : Unsigned_32) is
|
||||||
|
State : Manager;
|
||||||
|
Handle, Replacement : Word;
|
||||||
|
Result : Status;
|
||||||
|
Item : Message;
|
||||||
|
procedure Out_Byte (Port : Unsigned_16; Value : Unsigned_8) is
|
||||||
|
begin
|
||||||
|
Asm ("outb %0, %1", Inputs => (Unsigned_8'Asm_Input ("a", Value),
|
||||||
|
Unsigned_16'Asm_Input ("Nd", Port)), Volatile => True);
|
||||||
|
end Out_Byte;
|
||||||
|
function In_Byte (Port : Unsigned_16) return Unsigned_8 is
|
||||||
|
Value : Unsigned_8;
|
||||||
|
begin
|
||||||
|
Asm ("inb %1, %0", Outputs => Unsigned_8'Asm_Output ("=a", Value),
|
||||||
|
Inputs => Unsigned_16'Asm_Input ("Nd", Port), Volatile => True);
|
||||||
|
return Value;
|
||||||
|
end In_Byte;
|
||||||
|
procedure Line (Text : String) is
|
||||||
|
Full_Text : constant String := Text & ASCII.CR & ASCII.LF;
|
||||||
|
begin
|
||||||
|
for C of Full_Text loop
|
||||||
|
for Attempt in 1 .. 10_000 loop
|
||||||
|
exit when (In_Byte (16#3FD#) and 16#20#) /= 0;
|
||||||
|
end loop;
|
||||||
|
Out_Byte (16#3F8#, Unsigned_8 (Character'Pos (C)));
|
||||||
|
end loop;
|
||||||
|
end Line;
|
||||||
|
procedure Finish (Success : Boolean) with No_Return;
|
||||||
|
procedure Finish (Success : Boolean) is
|
||||||
|
Code : constant Unsigned_32 := (if Success then 16#10# else 16#11#);
|
||||||
|
begin
|
||||||
|
if Success then Line ("AGILA_BOOT_OK"); else Line ("AGILA_BOOT_FAILED"); end if;
|
||||||
|
Asm ("outl %0, %1", Inputs => (Unsigned_32'Asm_Input ("a", Code),
|
||||||
|
Unsigned_16'Asm_Input ("Nd", 16#F4#)), Volatile => True);
|
||||||
|
loop Asm ("cli; hlt", Volatile => True); end loop;
|
||||||
|
end Finish;
|
||||||
|
procedure Check (Condition : Boolean) is
|
||||||
|
begin
|
||||||
|
if not Condition then Finish (False); end if;
|
||||||
|
end Check;
|
||||||
|
begin
|
||||||
|
Out_Byte (16#3F9#, 0); Out_Byte (16#3FB#, 16#80#);
|
||||||
|
Out_Byte (16#3F8#, 3); Out_Byte (16#3F9#, 0);
|
||||||
|
Out_Byte (16#3FB#, 3); Out_Byte (16#3FA#, 16#C7#);
|
||||||
|
Out_Byte (16#3FC#, 16#0B#);
|
||||||
|
Line ("OPEN_AGILA_X86_64_ADA");
|
||||||
|
Check (Magic = 16#2BADB002#);
|
||||||
|
Create (State, 10, Handle, Result); Check (Result = Ok);
|
||||||
|
Send (State, Handle, 20, 42, Result); Check (Result = Permission_Denied);
|
||||||
|
Allow_Sender (State, Handle, 10, 20, Result); Check (Result = Ok);
|
||||||
|
for I in 1 .. Queue_Capacity loop
|
||||||
|
Send (State, Handle, 20, Word (I), Result); Check (Result = Ok);
|
||||||
|
end loop;
|
||||||
|
Send (State, Handle, 20, 99, Result); Check (Result = Full);
|
||||||
|
for I in 1 .. Queue_Capacity loop
|
||||||
|
Receive (State, Handle, 10, Item, Result);
|
||||||
|
Check (Result = Ok and Item.Value = Word (I) and Item.Sender = 20);
|
||||||
|
end loop;
|
||||||
|
Receive (State, Handle, 10, Item, Result); Check (Result = Empty);
|
||||||
|
Close (State, Handle, 10, Result); Check (Result = Ok);
|
||||||
|
Create (State, 30, Replacement, Result); Check (Result = Ok and Replacement /= Handle);
|
||||||
|
Send (State, Handle, 10, 1, Result); Check (Result = Invalid_Handle);
|
||||||
|
Line ("ADA_PORTS_BOOT_TESTS_OK");
|
||||||
|
Line ("Boot milestone: one address space; no user services or desktop yet.");
|
||||||
|
Finish (True);
|
||||||
|
end Boot_Main;
|
||||||
@@ -0,0 +1,3 @@
|
|||||||
|
with Interfaces;
|
||||||
|
procedure Boot_Main (Magic : Interfaces.Unsigned_32)
|
||||||
|
with Export, Convention => C, External_Name => "agila_boot_main", No_Return;
|
||||||
@@ -0,0 +1,8 @@
|
|||||||
|
set timeout=0
|
||||||
|
set default=0
|
||||||
|
serial --unit=0 --speed=38400
|
||||||
|
terminal_output serial
|
||||||
|
menuentry "Open Agila Ada boot milestone" {
|
||||||
|
multiboot /boot/open-agila.elf
|
||||||
|
boot
|
||||||
|
}
|
||||||
@@ -0,0 +1,9 @@
|
|||||||
|
ENTRY(_start)
|
||||||
|
SECTIONS {
|
||||||
|
. = 1M;
|
||||||
|
.text ALIGN(4K) : { KEEP(*(.multiboot)) *(.text.boot) *(.text*) }
|
||||||
|
.rodata ALIGN(4K) : { *(.rodata*) }
|
||||||
|
.data ALIGN(4K) : { *(.data*) }
|
||||||
|
.bss ALIGN(4K) : { *(COMMON) *(.bss*) }
|
||||||
|
/DISCARD/ : { *(.eh_frame*) *(.comment) *(.note*) }
|
||||||
|
}
|
||||||
@@ -0,0 +1,18 @@
|
|||||||
|
/* Freestanding compiler support, not an allocator or a VM subsystem. */
|
||||||
|
#include <stddef.h>
|
||||||
|
void *memset(void *dst,int value,size_t count) {
|
||||||
|
unsigned char *d=dst;
|
||||||
|
for(size_t i=0;i<count;i++)d[i]=(unsigned char)value;
|
||||||
|
return dst;
|
||||||
|
}
|
||||||
|
void *memcpy(void *dst,const void *src,size_t count) {
|
||||||
|
unsigned char *d=dst;const unsigned char *s=src;
|
||||||
|
for(size_t i=0;i<count;i++)d[i]=s[i];
|
||||||
|
return dst;
|
||||||
|
}
|
||||||
|
void *memmove(void *dst,const void *src,size_t count) {
|
||||||
|
unsigned char *d=dst;const unsigned char *s=src;
|
||||||
|
if((size_t)d<(size_t)s){for(size_t i=0;i<count;i++)d[i]=s[i];}
|
||||||
|
else {while(count){count--;d[count]=s[count];}}
|
||||||
|
return dst;
|
||||||
|
}
|
||||||
@@ -0,0 +1,83 @@
|
|||||||
|
/* Original Open Agila Multiboot v1 entry. QEMU x86-64/BIOS target only. */
|
||||||
|
.section .multiboot,"a"
|
||||||
|
.balign 4
|
||||||
|
.long 0x1badb002
|
||||||
|
.long 0x00000003
|
||||||
|
.long -(0x1badb002 + 0x00000003)
|
||||||
|
.section .text.boot,"ax"
|
||||||
|
.code32
|
||||||
|
.global _start
|
||||||
|
.type _start,@function
|
||||||
|
_start:
|
||||||
|
cli
|
||||||
|
cld
|
||||||
|
mov %eax, boot_magic
|
||||||
|
mov $stack_top, %esp
|
||||||
|
/* GRUB enters 32-bit protected mode. Map the first GiB with 2 MiB pages.
|
||||||
|
These writable executable boot mappings are NOT process isolation. */
|
||||||
|
mov $pdpt, %eax
|
||||||
|
or $3, %eax
|
||||||
|
mov %eax, pml4
|
||||||
|
mov $page_directory, %eax
|
||||||
|
or $3, %eax
|
||||||
|
mov %eax, pdpt
|
||||||
|
xor %ecx, %ecx
|
||||||
|
1:
|
||||||
|
mov %ecx, %eax
|
||||||
|
shl $21, %eax
|
||||||
|
or $0x83, %eax
|
||||||
|
mov %eax, page_directory(,%ecx,8)
|
||||||
|
inc %ecx
|
||||||
|
cmp $512, %ecx
|
||||||
|
jne 1b
|
||||||
|
mov %cr4, %eax
|
||||||
|
or $0x20, %eax
|
||||||
|
mov %eax, %cr4
|
||||||
|
mov $pml4, %eax
|
||||||
|
mov %eax, %cr3
|
||||||
|
mov $0xc0000080, %ecx
|
||||||
|
rdmsr
|
||||||
|
or $0x100, %eax
|
||||||
|
wrmsr
|
||||||
|
lgdt gdt_pointer
|
||||||
|
mov %cr0, %eax
|
||||||
|
or $0x80000000, %eax
|
||||||
|
mov %eax, %cr0
|
||||||
|
ljmp $0x08, $long_mode
|
||||||
|
.code64
|
||||||
|
long_mode:
|
||||||
|
mov $0x10, %ax
|
||||||
|
mov %ax, %ds
|
||||||
|
mov %ax, %es
|
||||||
|
mov %ax, %ss
|
||||||
|
xor %eax, %eax
|
||||||
|
mov %ax, %fs
|
||||||
|
mov %ax, %gs
|
||||||
|
mov $stack_top, %rsp
|
||||||
|
xor %rbp, %rbp
|
||||||
|
mov boot_magic(%rip), %edi
|
||||||
|
call agila_boot_main
|
||||||
|
2: cli
|
||||||
|
hlt
|
||||||
|
jmp 2b
|
||||||
|
.section .rodata,"a"
|
||||||
|
.balign 8
|
||||||
|
gdt:
|
||||||
|
.quad 0
|
||||||
|
.quad 0x00af9a000000ffff
|
||||||
|
.quad 0x00cf92000000ffff
|
||||||
|
gdt_end:
|
||||||
|
gdt_pointer:
|
||||||
|
.word gdt_end-gdt-1
|
||||||
|
.long gdt
|
||||||
|
.section .bss,"aw",@nobits
|
||||||
|
.balign 4
|
||||||
|
boot_magic: .skip 4
|
||||||
|
.balign 4096
|
||||||
|
pml4: .skip 4096
|
||||||
|
pdpt: .skip 4096
|
||||||
|
page_directory: .skip 4096
|
||||||
|
.balign 16
|
||||||
|
stack_bottom: .skip 65536
|
||||||
|
stack_top:
|
||||||
|
.section .note.GNU-stack,"",@progbits
|
||||||
@@ -0,0 +1,116 @@
|
|||||||
|
package body Agila_Ports is
|
||||||
|
use type Word;
|
||||||
|
Max_Generation : constant Word := Word'Last / Max_Ports;
|
||||||
|
function Valid (State : Manager; Handle : Word) return Boolean is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
return Handle >= Max_Ports
|
||||||
|
and then State.Table (Slot).Active
|
||||||
|
and then State.Table (Slot).Generation = Handle / Max_Ports;
|
||||||
|
end Valid;
|
||||||
|
|
||||||
|
procedure Create (State : in out Manager; Owner : Word;
|
||||||
|
Handle : out Word; Result : out Status) is
|
||||||
|
begin
|
||||||
|
Handle := 0;
|
||||||
|
if Owner = 0 then Result := Invalid_Argument; return; end if;
|
||||||
|
for Slot in State.Table'Range loop
|
||||||
|
if not State.Table (Slot).Active and not State.Table (Slot).Retired then
|
||||||
|
State.Table (Slot).Active := True;
|
||||||
|
State.Table (Slot).Owner := Owner;
|
||||||
|
State.Table (Slot).Allowed_Sender := 0;
|
||||||
|
State.Table (Slot).Head := 0;
|
||||||
|
State.Table (Slot).Count := 0;
|
||||||
|
State.Table (Slot).Queue := [others => (0, 0)];
|
||||||
|
Handle := State.Table (Slot).Generation * Max_Ports + Word (Slot);
|
||||||
|
Result := Ok;
|
||||||
|
return;
|
||||||
|
end if;
|
||||||
|
end loop;
|
||||||
|
Result := Exhausted;
|
||||||
|
end Create;
|
||||||
|
|
||||||
|
procedure Allow_Sender (State : in out Manager; Handle, Owner, Sender : Word;
|
||||||
|
Result : out Status) is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
if not Valid (State, Handle) then Result := Invalid_Handle;
|
||||||
|
elsif State.Table (Slot).Owner /= Owner then Result := Permission_Denied;
|
||||||
|
elsif Sender = 0 then Result := Invalid_Argument;
|
||||||
|
else State.Table (Slot).Allowed_Sender := Sender; Result := Ok;
|
||||||
|
end if;
|
||||||
|
end Allow_Sender;
|
||||||
|
|
||||||
|
procedure Revoke_Sender (State : in out Manager; Handle, Owner, Sender : Word;
|
||||||
|
Result : out Status) is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
if not Valid (State, Handle) then Result := Invalid_Handle;
|
||||||
|
elsif State.Table (Slot).Owner /= Owner then Result := Permission_Denied;
|
||||||
|
elsif Sender = 0 or else State.Table (Slot).Allowed_Sender /= Sender then
|
||||||
|
Result := Invalid_Argument;
|
||||||
|
else State.Table (Slot).Allowed_Sender := 0; Result := Ok;
|
||||||
|
end if;
|
||||||
|
end Revoke_Sender;
|
||||||
|
|
||||||
|
procedure Send (State : in out Manager; Handle, Caller, Value : Word;
|
||||||
|
Result : out Status) is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
if not Valid (State, Handle) then Result := Invalid_Handle; return; end if;
|
||||||
|
declare
|
||||||
|
P : Port renames State.Table (Slot);
|
||||||
|
begin
|
||||||
|
if Caller = 0 or else (Caller /= P.Owner and Caller /= P.Allowed_Sender) then
|
||||||
|
Result := Permission_Denied;
|
||||||
|
elsif P.Count = Queue_Capacity then Result := Full;
|
||||||
|
else
|
||||||
|
P.Queue ((P.Head + P.Count) mod Queue_Capacity) := (Caller, Value);
|
||||||
|
P.Count := P.Count + 1;
|
||||||
|
Result := Ok;
|
||||||
|
end if;
|
||||||
|
end;
|
||||||
|
end Send;
|
||||||
|
|
||||||
|
procedure Receive (State : in out Manager; Handle, Caller : Word;
|
||||||
|
Item : out Message; Result : out Status) is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
Item := (0, 0);
|
||||||
|
if not Valid (State, Handle) then Result := Invalid_Handle; return; end if;
|
||||||
|
declare
|
||||||
|
P : Port renames State.Table (Slot);
|
||||||
|
begin
|
||||||
|
if Caller /= P.Owner then Result := Permission_Denied;
|
||||||
|
elsif P.Count = 0 then Result := Empty;
|
||||||
|
else
|
||||||
|
Item := P.Queue (P.Head);
|
||||||
|
P.Queue (P.Head) := (0, 0);
|
||||||
|
P.Head := (P.Head + 1) mod Queue_Capacity;
|
||||||
|
P.Count := P.Count - 1;
|
||||||
|
Result := Ok;
|
||||||
|
end if;
|
||||||
|
end;
|
||||||
|
end Receive;
|
||||||
|
|
||||||
|
procedure Close (State : in out Manager; Handle, Caller : Word;
|
||||||
|
Result : out Status) is
|
||||||
|
Slot : constant Natural := Natural (Handle mod Max_Ports);
|
||||||
|
begin
|
||||||
|
if not Valid (State, Handle) then Result := Invalid_Handle;
|
||||||
|
elsif State.Table (Slot).Owner /= Caller then Result := Permission_Denied;
|
||||||
|
else
|
||||||
|
State.Table (Slot).Active := False;
|
||||||
|
State.Table (Slot).Owner := 0;
|
||||||
|
State.Table (Slot).Allowed_Sender := 0;
|
||||||
|
State.Table (Slot).Count := 0;
|
||||||
|
State.Table (Slot).Queue := [others => (0, 0)];
|
||||||
|
if State.Table (Slot).Generation = Max_Generation then
|
||||||
|
State.Table (Slot).Retired := True;
|
||||||
|
else
|
||||||
|
State.Table (Slot).Generation := State.Table (Slot).Generation + 1;
|
||||||
|
end if;
|
||||||
|
Result := Ok;
|
||||||
|
end if;
|
||||||
|
end Close;
|
||||||
|
end Agila_Ports;
|
||||||
@@ -0,0 +1,43 @@
|
|||||||
|
with Interfaces;
|
||||||
|
package Agila_Ports is
|
||||||
|
-- Original Open Agila implementation. Host identity values are supplied by
|
||||||
|
-- trusted callers; a future syscall boundary must derive identity itself.
|
||||||
|
subtype Word is Interfaces.Unsigned_32;
|
||||||
|
Max_Ports : constant := 8;
|
||||||
|
Queue_Capacity : constant := 4;
|
||||||
|
type Status is (Ok, Invalid_Handle, Permission_Denied, Full, Empty,
|
||||||
|
Exhausted, Invalid_Argument);
|
||||||
|
type Message is record
|
||||||
|
Sender : Word := 0;
|
||||||
|
Value : Word := 0;
|
||||||
|
end record;
|
||||||
|
type Manager is limited private;
|
||||||
|
procedure Create (State : in out Manager; Owner : Word;
|
||||||
|
Handle : out Word; Result : out Status);
|
||||||
|
procedure Allow_Sender (State : in out Manager; Handle, Owner, Sender : Word;
|
||||||
|
Result : out Status);
|
||||||
|
procedure Revoke_Sender (State : in out Manager; Handle, Owner, Sender : Word;
|
||||||
|
Result : out Status);
|
||||||
|
procedure Send (State : in out Manager; Handle, Caller, Value : Word;
|
||||||
|
Result : out Status);
|
||||||
|
procedure Receive (State : in out Manager; Handle, Caller : Word;
|
||||||
|
Item : out Message; Result : out Status);
|
||||||
|
procedure Close (State : in out Manager; Handle, Caller : Word;
|
||||||
|
Result : out Status);
|
||||||
|
private
|
||||||
|
type Messages is array (Natural range 0 .. Queue_Capacity - 1) of Message;
|
||||||
|
type Port is record
|
||||||
|
Active : Boolean := False;
|
||||||
|
Retired : Boolean := False;
|
||||||
|
Generation : Word := 1;
|
||||||
|
Owner : Word := 0;
|
||||||
|
Allowed_Sender : Word := 0;
|
||||||
|
Head : Natural range 0 .. Queue_Capacity - 1 := 0;
|
||||||
|
Count : Natural range 0 .. Queue_Capacity := 0;
|
||||||
|
Queue : Messages := [others => (0, 0)];
|
||||||
|
end record;
|
||||||
|
type Ports is array (Natural range 0 .. Max_Ports - 1) of Port;
|
||||||
|
type Manager is limited record
|
||||||
|
Table : Ports;
|
||||||
|
end record;
|
||||||
|
end Agila_Ports;
|
||||||
@@ -0,0 +1,52 @@
|
|||||||
|
# Open Agila architecture direction
|
||||||
|
|
||||||
|
Status: original implementation, early boot and host-port milestone. This document separates implemented mechanisms from the proposed architecture.
|
||||||
|
|
||||||
|
## Design references
|
||||||
|
|
||||||
|
[OpenStep](https://www.gnustep.org/resources/OpenStepSpec/OpenStepIntro/TXT.html) describes an OS-independent object-oriented application layer, including Foundation and Application Kit. Agila will define its own Ada/V framework contracts first; compatibility requires separately scoped conformance tests.
|
||||||
|
|
||||||
|
[MINIX architecture](https://wiki.minix3.org/doku.php?id=developersguide:overviewofminixarchitecture) separates a small privileged kernel from user-mode drivers and services, with explicit communication and authority checks. Open Agila's target is a small kernel and restartable services, not reuse of MINIX code or its exact IPC ABI.
|
||||||
|
|
||||||
|
The owner has a specific Open Amiga repository. Its URL/path, license, APIs, and tested targets are pending. No alternative project has been substituted, and no integration or compatibility claim is made.
|
||||||
|
|
||||||
|
## Target structure
|
||||||
|
|
||||||
|
```mermaid
|
||||||
|
flowchart TD
|
||||||
|
Apps[Applications in V / Flying V and Ada] --> Frameworks[Agila application and foundation contracts]
|
||||||
|
Frameworks --> Services[User services: UI, files, network, audio]
|
||||||
|
Services --> IPC[Versioned IPC and scoped resource grants]
|
||||||
|
IPC --> Kernel[Ada kernel: address spaces, scheduling, IPC, interrupts]
|
||||||
|
Drivers[User device drivers] --> IPC
|
||||||
|
Kernel --> Hardware[CPU, memory and devices]
|
||||||
|
```
|
||||||
|
|
||||||
|
Only the bounded port mechanism and minimal boot path are implemented here. The service, syscall, framework, scheduler, and driver layers in this diagram are future work.
|
||||||
|
|
||||||
|
## Current mechanism
|
||||||
|
|
||||||
|
`Agila_Ports.Manager` owns eight independent ports. Each holds four `(sender, value)` messages. Operations are non-blocking: a full queue returns `Full`; an empty queue returns `Empty`. Each port has an owner and at most one additional allowed sender. Only the owner can receive, grant, revoke, or close. Granting a different sender replaces the previous extra grant. Revocation prevents future sends; already queued messages remain queued.
|
||||||
|
|
||||||
|
The handle encodes a slot and generation. Closing clears queued data and advances the generation. A stale handle cannot address a reopened port. A slot retires at generation exhaustion instead of wrapping and making an ancient handle valid again. This is a reference-validity mechanism, not an unforgeable capability.
|
||||||
|
|
||||||
|
The host adapter accepts identity integers from its caller and stores a single global manager. It is deliberately single-threaded. A real syscall boundary must derive the caller from trusted scheduler state, validate user buffers, and synchronize shared state. An application that can choose its own identity can impersonate another caller in this demonstration.
|
||||||
|
|
||||||
|
## Boot boundary
|
||||||
|
|
||||||
|
The BIOS/Multiboot entry starts in 32-bit mode, installs a GDT, creates temporary identity mappings for the first GiB, enables long mode, establishes a stack, and calls Ada. It assumes an x86-64-capable target. The mapping uses writable, executable 2 MiB pages and does not establish user/kernel protection.
|
||||||
|
|
||||||
|
The Ada entry verifies the Multiboot magic and exercises the port core before reporting success. The small C file only supplies compiler memory-copy/fill routines; it is not a memory allocator. Runtime checks remain enabled in host tests. The bare-metal build suppresses GNAT runtime checks because exception handling and the runtime are not yet ported. Explicit boot test conditions remain active. This is not a proof that every unchecked Ada execution is safe.
|
||||||
|
|
||||||
|
## Language roles
|
||||||
|
|
||||||
|
- Ada: explicit kernel data structures and policies, bounded operations, contracts/tests, later scheduling and memory mechanisms.
|
||||||
|
- Standard V: host tools and initial application/service clients through documented interfaces.
|
||||||
|
- Flying V: a separate Agila application language, used only through its actual published SDK/toolchain contracts.
|
||||||
|
- Assembly and minimal C: necessary startup/ABI support, kept small and reviewed.
|
||||||
|
|
||||||
|
Future service interfaces should use versioned fixed-width fields and validated lengths rather than exposing Ada record layouts, V objects, host pointers, or compiler-specific enums across address spaces.
|
||||||
|
|
||||||
|
## Evidence before claims
|
||||||
|
|
||||||
|
A host check demonstrates data-structure behavior under a host runtime. A QEMU boot check demonstrates a particular virtual machine and code path. Neither proves user-mode isolation, fault recovery, compatibility, or physical-device support. Those require the explicit tests in the roadmap.
|
||||||
@@ -0,0 +1,26 @@
|
|||||||
|
Build Open Agila and grow its developer community
|
||||||
|
|
||||||
|
Objective
|
||||||
|
Develop Open Agila into a reproducibly buildable, open operating system, primarily in Ada and V. Use OpenStep as an application-framework reference and MINIX as a reference for a small kernel, explicit IPC, least authority, and restartable services. Inspect the specific Open Amiga repository supplied by the owner before deciding what to integrate. Do not substitute AROS or a different Amiga project without that evidence.
|
||||||
|
|
||||||
|
Begin with the existing Agila Forge repositories and preserve their history, licenses, and working behavior. Keep Open Agila development distinct from private Agila OS components. Do not publish private source, credentials, or unexplained third-party binaries. Keep Flying V distinct from standard V and use its actual compiler/SDK contracts.
|
||||||
|
|
||||||
|
Build in verifiable milestones
|
||||||
|
1. Audit current code and publish an architecture, source inventory, supported-target matrix, and backlog with testable acceptance criteria.
|
||||||
|
2. Make the existing host build repeatable. Implement a bounded Ada message-port core, explicit access checks, and a V client through a documented ABI. Test errors, capacity limits, stale handles, and invalid requests as well as successful behavior.
|
||||||
|
3. Produce a minimal x86-64 QEMU boot target with serial output and a bounded smoke test. Clearly distinguish bare-metal boot evidence from host simulations.
|
||||||
|
4. Progress toward memory management, exception/interrupt handling, scheduling, separate address spaces, IPC syscalls, restartable user services, storage, networking, and device drivers. State what is implemented, simulated, untested, or planned. Add real isolation tests before describing a service as isolated.
|
||||||
|
5. Build the application/runtime layer and OpenStep-informed framework contracts in Ada and V/Flying V. Develop compatibility only against an identified specification and executable conformance tests. Integrate the owner's Open Amiga source only after reviewing its APIs, provenance, and license.
|
||||||
|
6. Add CPU/GPU topology, memory mappings, synchronization, and measured workload placement as hardware support becomes available. Label simulated measurements and untested hardware honestly.
|
||||||
|
|
||||||
|
Expand Agila Forge
|
||||||
|
Publish working source, build instructions, examples, tests, architecture decisions, and contribution guides. Organize real starter tasks and larger milestones with acceptance criteria. Make it easy for a new developer to clone, build, reproduce a test, submit a patch, and explain the result. Preserve the restored repositories and hosting protections. Do not enable execution of untrusted CI jobs on the production Forge host.
|
||||||
|
|
||||||
|
Expand Agila University
|
||||||
|
Turn each verified implementation milestone into English, Tagalog, and Bisaya lessons of approximately 15 minutes, with runnable browser exercises where supported, automated checks, feedback, and links to the exact source. Retain lesson and track completion certificates. Connect learning tracks to projects and real Forge contributions. A certificate records completed checks; tested code, explanations, documentation, and portfolio work provide additional evidence of skill. No human mentor is required for lesson progression.
|
||||||
|
|
||||||
|
Definition of progress
|
||||||
|
Report exact commits, reproducible commands, test results, supported targets, and remaining work. Do not call a host prototype a bootable OS, a boot demo a complete operating system, or a model a measured hardware result. Avoid promises of full compatibility or professional mastery without evidence. Continue useful independent work while a specific integration detail is awaiting clarification.
|
||||||
|
|
||||||
|
Long-term success
|
||||||
|
A growing pool of developers can independently understand, test, maintain, and extend Open Agila: applications, websites, server systems, OS components, and AI runtimes. Judge success through working contributions and understanding, including the ability to review AI-generated code.
|
||||||
@@ -0,0 +1,15 @@
|
|||||||
|
# Host port ABI v0
|
||||||
|
|
||||||
|
This ABI exists to test Ada/V interoperability. It is not a syscall ABI and is not stable for production applications.
|
||||||
|
|
||||||
|
The C header in `include/agila_ports.h` is the shared declaration. All identity, handle, and message-value fields are `uint32_t`. Status values are C `int`: 0 success, 1 invalid handle, 2 permission denied, 3 full, 4 empty, 5 exhausted, 6 invalid argument. The Ada library uses GNAT's automatic elaboration for a shared standalone library.
|
||||||
|
|
||||||
|
`agila_port_create(owner)` returns a nonzero handle or zero if the owner is zero or every slot is active/retired. The core Ada API distinguishes those failures; the initial host wrapper intentionally has the smaller return shape.
|
||||||
|
|
||||||
|
The owner can grant one additional sender, replace that sender, revoke that exact grant, receive, and close. The owner retains its own send permission. Sender zero is invalid. Revocation does not remove accepted messages. Closing clears the queue and invalidates the handle. A rejected operation does not insert or remove a message.
|
||||||
|
|
||||||
|
`agila_port_receive(handle, caller, value)` requires either a valid writable pointer to a `uint32_t`, or NULL. NULL returns invalid argument. On other failures a valid output pointer receives zero. Arbitrary invalid pointers are outside this trusted host ABI contract; the wrapper does not attempt to probe application memory. A future kernel API must validate/copy user buffers through a different boundary.
|
||||||
|
|
||||||
|
Calls must be serialized by the host application. The library does not implement locking, separate processes, caller authentication, transport, persistence, or shared-memory ownership. The generation-checked handle is not a secret authorization token.
|
||||||
|
|
||||||
|
The V demonstration covers denied sends, grant, send/receive, revocation, close, and stale-reference rejection. The C test covers NULL and full-width unsigned values. The Ada tests cover ring wrap, FIFO order, exhaustion, permission failures, and independent ports.
|
||||||
@@ -0,0 +1,28 @@
|
|||||||
|
# Roadmap and acceptance evidence
|
||||||
|
|
||||||
|
Each milestone should include source, tests, an exact build command, and an accompanying University lesson. The remaining work is substantial; the first boot milestone is not a complete OS.
|
||||||
|
|
||||||
|
| Milestone | State | Acceptance evidence |
|
||||||
|
| --- | --- | --- |
|
||||||
|
| M0: honest source inventory and host build | Implemented | `make run` accurately reports placeholders; build instructions reproduce |
|
||||||
|
| M1: bounded Ada ports and V interoperability | Implemented | `make test` passes normal, denied, boundary, stale-reference, and ABI checks |
|
||||||
|
| M2: x86-64 virtual-machine boot | Implemented | `make boot-test` checks long-mode Ada entry, shared port-core tests, serial proof and exit status |
|
||||||
|
| M3: exceptions and physical-memory inventory | Planned | Controlled exceptions produce structured diagnostics; parse Multiboot memory data with bounds; never allocate reserved/kernel/page-table/stack regions |
|
||||||
|
| M4: page allocator and protected address spaces | Planned | Reuse/free exhaustion tests; read-only and unmapped access faults; separate users cannot read each other's pages; executable/write policies defined |
|
||||||
|
| M5: timer, context switching and scheduling | Planned | Two tasks make progress; register/context preservation; bounded queues; starvation/cancellation cases documented |
|
||||||
|
| M6: syscall IPC and service restart | Planned | Identity comes from trusted task state; invalid user pointers fail safely; service crash/restart does not corrupt another service; stale endpoint references fail |
|
||||||
|
| M7: storage, network and devices | Planned | Disposable virtual disk/network tests; crash/recovery and corruption cases; no physical-disk experiments without explicit approval |
|
||||||
|
| M8: application/framework contracts | Planned | Versioned Ada/V APIs, event loop, lifetime rules, serialization tests, and a working sample application |
|
||||||
|
| M9: Open Amiga integration | Awaiting source | Identify owner's repository, license, architecture and build; choose bounded component and test compatibility explicitly |
|
||||||
|
| M10: additional ISAs and CPU/GPU placement | Planned | Independent target boots, measured topology/transfer/latency evidence, synchronization tests; unsupported targets clearly labeled |
|
||||||
|
|
||||||
|
## Useful first contributions
|
||||||
|
|
||||||
|
1. Add an independently written randomized FIFO reference-model test and demonstrate that a deliberate queue bug is caught.
|
||||||
|
2. Test replacement of an allowed sender and the policy for messages already queued before revocation.
|
||||||
|
3. Add a boot-failure fixture or reproducible fault injection so the smoke test is shown to reject a false pass.
|
||||||
|
4. Improve translated build instructions with actual commands and captured output from a clean machine.
|
||||||
|
5. Design bounded parsing of the bootloader memory map with malformed/truncated fixtures before touching an allocator.
|
||||||
|
6. Specify a versioned service-message format with length, operation, request ID, and serialization test vectors.
|
||||||
|
|
||||||
|
Every task should identify the relevant files, expected behavior, tests to run, and limits. Review must assess whether evidence establishes the claimed property, not just whether a demo prints a success message.
|
||||||
@@ -0,0 +1,34 @@
|
|||||||
|
# Milestone validation — 1 November 2026
|
||||||
|
|
||||||
|
Target: Ubuntu 24.04 x86-64 development environment; GCC/GNAT 13; V 0.5.2 (`7647ce1`); QEMU TCG, `qemu64`, one virtual CPU, 64 MiB guest memory, BIOS/GRUB Multiboot. Builds and QEMU ran as an unprivileged account, not as the web or Forge service.
|
||||||
|
|
||||||
|
Commands:
|
||||||
|
|
||||||
|
```sh
|
||||||
|
make test V=/opt/agila-v/v
|
||||||
|
make boot-test
|
||||||
|
```
|
||||||
|
|
||||||
|
Observed host results:
|
||||||
|
|
||||||
|
```text
|
||||||
|
ADA_PORTS_OK: FIFO, wrap, full/empty, grants, revocation, stale handles, exhaustion, port separation
|
||||||
|
ADA_V_PORTS_OK value=42
|
||||||
|
Host ABI demo: caller IDs are trusted inputs; no process isolation is claimed.
|
||||||
|
```
|
||||||
|
|
||||||
|
The C ABI test exited successfully after checking NULL output, full-width unsigned payload, empty output, and close behavior. Host Ada checks and overflow checks were enabled.
|
||||||
|
|
||||||
|
Observed virtual-machine result:
|
||||||
|
|
||||||
|
```text
|
||||||
|
OPEN_AGILA_X86_64_ADA
|
||||||
|
ADA_PORTS_BOOT_TESTS_OK
|
||||||
|
Boot milestone: one address space; no user services or desktop yet.
|
||||||
|
AGILA_BOOT_OK
|
||||||
|
QEMU_BOOT_SMOKE_PASS
|
||||||
|
```
|
||||||
|
|
||||||
|
QEMU exited with status 33, the success code produced by the configured debug-exit device. The smoke test requires that exit status and all three success markers. It fails on timeout, a missing image, a wrong exit status, or missing proof text.
|
||||||
|
|
||||||
|
This validates the listed code paths on this virtual-machine target. It does not validate user-space isolation, arbitrary input pointers, concurrent callers, generation-counter exhaustion after hundreds of millions of closes, UEFI, physical hardware, other ISAs, GPU work, or framework compatibility.
|
||||||
@@ -0,0 +1,29 @@
|
|||||||
|
module main
|
||||||
|
#flag -I @VMODROOT/include
|
||||||
|
#flag -L @VMODROOT/build/lib
|
||||||
|
#flag -lagila_host
|
||||||
|
#include "agila_ports.h"
|
||||||
|
fn C.agila_port_create(u32) u32
|
||||||
|
fn C.agila_port_allow_sender(u32,u32,u32) int
|
||||||
|
fn C.agila_port_revoke_sender(u32,u32,u32) int
|
||||||
|
fn C.agila_port_send(u32,u32,u32) int
|
||||||
|
fn C.agila_port_receive(u32,u32,&u32) int
|
||||||
|
fn C.agila_port_close(u32,u32) int
|
||||||
|
fn main() {
|
||||||
|
owner := u32(10)
|
||||||
|
worker := u32(20)
|
||||||
|
port := C.agila_port_create(owner)
|
||||||
|
assert port != 0
|
||||||
|
assert C.agila_port_send(port,worker,42) == 2 // denied until owner grants
|
||||||
|
assert C.agila_port_allow_sender(port,owner,worker) == 0
|
||||||
|
assert C.agila_port_send(port,worker,42) == 0
|
||||||
|
mut value := u32(0)
|
||||||
|
assert C.agila_port_receive(port,owner,&value) == 0
|
||||||
|
assert value == 42
|
||||||
|
assert C.agila_port_revoke_sender(port,owner,worker) == 0
|
||||||
|
assert C.agila_port_send(port,worker,7) == 2
|
||||||
|
assert C.agila_port_close(port,owner) == 0
|
||||||
|
assert C.agila_port_send(port,owner,7) == 1
|
||||||
|
println('ADA_V_PORTS_OK value=${value}')
|
||||||
|
println('Host ABI demo: caller IDs are trusted inputs; no process isolation is claimed.')
|
||||||
|
}
|
||||||
@@ -0,0 +1,13 @@
|
|||||||
|
project Host_Library is
|
||||||
|
for Languages use ("Ada");
|
||||||
|
for Source_Dirs use ("core", "abi");
|
||||||
|
for Object_Dir use "build/library-obj";
|
||||||
|
for Library_Dir use "build/lib";
|
||||||
|
for Library_Name use "agila_host";
|
||||||
|
for Library_Kind use "dynamic";
|
||||||
|
for Library_Interface use ("Agila_ABI");
|
||||||
|
for Library_Auto_Init use "true";
|
||||||
|
package Compiler is
|
||||||
|
for Default_Switches ("Ada") use ("-gnat2022", "-gnata", "-gnatwa", "-gnato", "-fPIC");
|
||||||
|
end Compiler;
|
||||||
|
end Host_Library;
|
||||||
@@ -0,0 +1,17 @@
|
|||||||
|
#ifndef AGILA_PORTS_H
|
||||||
|
#define AGILA_PORTS_H
|
||||||
|
#include <stdint.h>
|
||||||
|
/* Host demonstration ABI v0: single-threaded, trusted caller identities.
|
||||||
|
* Not a syscall API. receive requires a valid writable pointer or NULL.
|
||||||
|
* A handle is a generation-checked reference, not an unforgeable capability.
|
||||||
|
* create returns 0 for invalid owner or exhausted capacity.
|
||||||
|
*/
|
||||||
|
enum agila_status { AGILA_OK=0, AGILA_INVALID_HANDLE=1, AGILA_DENIED=2,
|
||||||
|
AGILA_FULL=3, AGILA_EMPTY=4, AGILA_EXHAUSTED=5, AGILA_INVALID_ARGUMENT=6 };
|
||||||
|
uint32_t agila_port_create(uint32_t owner);
|
||||||
|
int agila_port_allow_sender(uint32_t handle,uint32_t owner,uint32_t sender);
|
||||||
|
int agila_port_revoke_sender(uint32_t handle,uint32_t owner,uint32_t sender);
|
||||||
|
int agila_port_send(uint32_t handle,uint32_t caller,uint32_t value);
|
||||||
|
int agila_port_receive(uint32_t handle,uint32_t caller,uint32_t *value);
|
||||||
|
int agila_port_close(uint32_t handle,uint32_t caller);
|
||||||
|
#endif
|
||||||
+7
-7
@@ -15,12 +15,12 @@ package body Kernel is
|
|||||||
Timer.Initialize;
|
Timer.Initialize;
|
||||||
Scheduler.Initialize;
|
Scheduler.Initialize;
|
||||||
|
|
||||||
Console.Write_Line ("Agila Open Kernel 0.1");
|
Console.Write_Line ("Open Agila 0.2 host scaffold");
|
||||||
Console.Write_Line ("CPU: initialized");
|
Console.Write_Line ("CPU: host placeholder");
|
||||||
Console.Write_Line ("Memory: initialized");
|
Console.Write_Line ("Memory: host placeholder");
|
||||||
Console.Write_Line ("Interrupts: initialized");
|
Console.Write_Line ("Interrupts: host placeholder");
|
||||||
Console.Write_Line ("Timer: initialized");
|
Console.Write_Line ("Timer: host placeholder");
|
||||||
Console.Write_Line ("Scheduler: initialized");
|
Console.Write_Line ("Scheduler: host placeholder");
|
||||||
Console.Write_Line ("System ready");
|
Console.Write_Line ("Host scaffold complete; this target is not a bootable OS");
|
||||||
end Start;
|
end Start;
|
||||||
end Kernel;
|
end Kernel;
|
||||||
@@ -0,0 +1,10 @@
|
|||||||
|
project Ports is
|
||||||
|
for Languages use ("Ada");
|
||||||
|
for Source_Dirs use ("core", "tests");
|
||||||
|
for Object_Dir use "build/ports-obj";
|
||||||
|
for Exec_Dir use "build/bin";
|
||||||
|
for Main use ("ports_test.adb");
|
||||||
|
package Compiler is
|
||||||
|
for Default_Switches ("Ada") use ("-gnat2022", "-gnata", "-gnatwa", "-gnato");
|
||||||
|
end Compiler;
|
||||||
|
end Ports;
|
||||||
@@ -0,0 +1,13 @@
|
|||||||
|
#!/usr/bin/env python3
|
||||||
|
"""A bounded, no-network QEMU test; no host disks are attached."""
|
||||||
|
import pathlib,subprocess,sys
|
||||||
|
image=pathlib.Path(sys.argv[1] if len(sys.argv)>1 else 'build/open-agila.iso').resolve()
|
||||||
|
if not image.is_file():raise SystemExit('Build the ISO first with make boot.')
|
||||||
|
command=['qemu-system-x86_64','-machine','pc,accel=tcg','-cpu','qemu64','-m','64M','-smp','1','-display','none','-serial','stdio','-monitor','none','-nic','none','-no-reboot','-no-shutdown','-device','isa-debug-exit,iobase=0xf4,iosize=0x04','-cdrom',str(image)]
|
||||||
|
try:result=subprocess.run(command,capture_output=True,text=True,timeout=30)
|
||||||
|
except subprocess.TimeoutExpired as error:
|
||||||
|
print((error.stdout or b'').decode(errors='replace') if isinstance(error.stdout,bytes) else error.stdout or '')
|
||||||
|
raise SystemExit('FAIL: boot did not finish within 30 seconds')
|
||||||
|
print(result.stdout,end='');print(result.stderr,end='',file=sys.stderr)
|
||||||
|
if result.returncode!=33 or 'OPEN_AGILA_X86_64_ADA' not in result.stdout or 'ADA_PORTS_BOOT_TESTS_OK' not in result.stdout or 'AGILA_BOOT_OK' not in result.stdout:raise SystemExit('FAIL: missing boot proof or wrong QEMU exit status: '+str(result.returncode))
|
||||||
|
print('QEMU_BOOT_SMOKE_PASS')
|
||||||
@@ -0,0 +1,13 @@
|
|||||||
|
#include "agila_ports.h"
|
||||||
|
#include <assert.h>
|
||||||
|
#include <stddef.h>
|
||||||
|
int main(void) {
|
||||||
|
uint32_t h=agila_port_create(1), value=123;
|
||||||
|
assert(h!=0);
|
||||||
|
assert(agila_port_receive(h,1,NULL)==AGILA_INVALID_ARGUMENT);
|
||||||
|
assert(agila_port_send(h,1,0xffffffffu)==AGILA_OK);
|
||||||
|
assert(agila_port_receive(h,1,&value)==AGILA_OK && value==0xffffffffu);
|
||||||
|
assert(agila_port_receive(h,1,&value)==AGILA_EMPTY && value==0);
|
||||||
|
assert(agila_port_close(h,1)==AGILA_OK);
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
@@ -0,0 +1,61 @@
|
|||||||
|
with Ada.Text_IO;
|
||||||
|
with Agila_Ports; use Agila_Ports;
|
||||||
|
procedure Ports_Test is
|
||||||
|
use type Word;
|
||||||
|
S : Manager;
|
||||||
|
H, New_H : Word;
|
||||||
|
R : Status;
|
||||||
|
M : Message;
|
||||||
|
Handles : array (1 .. Max_Ports) of Word;
|
||||||
|
begin
|
||||||
|
Create (S, 0, H, R); pragma Assert (R = Invalid_Argument and H = 0);
|
||||||
|
Create (S, 10, H, R); pragma Assert (R = Ok and H /= 0);
|
||||||
|
Receive (S, H, 10, M, R); pragma Assert (R = Empty and M = (0, 0));
|
||||||
|
Send (S, 0, 10, 1, R); pragma Assert (R = Invalid_Handle);
|
||||||
|
Send (S, Word'Last, 10, 1, R); pragma Assert (R = Invalid_Handle);
|
||||||
|
Send (S, H, 0, 1, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Send (S, H, 20, 1, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Allow_Sender (S, H, 99, 20, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Allow_Sender (S, H, 10, 0, R); pragma Assert (R = Invalid_Argument);
|
||||||
|
Allow_Sender (S, H, 10, 20, R); pragma Assert (R = Ok);
|
||||||
|
for I in 1 .. Queue_Capacity loop
|
||||||
|
Send (S, H, 20, Word (I), R); pragma Assert (R = Ok);
|
||||||
|
end loop;
|
||||||
|
Send (S, H, 20, 99, R); pragma Assert (R = Full);
|
||||||
|
Receive (S, H, 20, M, R); pragma Assert (R = Permission_Denied and M = (0, 0));
|
||||||
|
for I in 1 .. Queue_Capacity loop
|
||||||
|
Receive (S, H, 10, M, R); pragma Assert (R = Ok and M = (20, Word (I)));
|
||||||
|
end loop;
|
||||||
|
Receive (S, H, 10, M, R); pragma Assert (R = Empty);
|
||||||
|
-- Exercise wrap-around without emptying the queue between every operation.
|
||||||
|
for Cycle in 1 .. 100 loop
|
||||||
|
Send (S, H, 20, Word (Cycle), R); pragma Assert (R = Ok);
|
||||||
|
Send (S, H, 10, Word (Cycle + 100), R); pragma Assert (R = Ok);
|
||||||
|
Receive (S, H, 10, M, R); pragma Assert (R = Ok and M.Value = Word (Cycle));
|
||||||
|
Receive (S, H, 10, M, R); pragma Assert (R = Ok and M.Value = Word (Cycle + 100));
|
||||||
|
end loop;
|
||||||
|
Revoke_Sender (S, H, 99, 20, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Revoke_Sender (S, H, 10, 20, R); pragma Assert (R = Ok);
|
||||||
|
Send (S, H, 20, 8, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Close (S, H, 20, R); pragma Assert (R = Permission_Denied);
|
||||||
|
Send (S, H, 10, 123, R); pragma Assert (R = Ok);
|
||||||
|
Close (S, H, 10, R); pragma Assert (R = Ok);
|
||||||
|
Create (S, 30, New_H, R); pragma Assert (R = Ok and New_H /= H);
|
||||||
|
Send (S, H, 10, 5, R); pragma Assert (R = Invalid_Handle);
|
||||||
|
Allow_Sender (S, H, 10, 20, R); pragma Assert (R = Invalid_Handle);
|
||||||
|
Receive (S, New_H, 30, M, R); pragma Assert (R = Empty);
|
||||||
|
Close (S, New_H, 30, R); pragma Assert (R = Ok);
|
||||||
|
for I in Handles'Range loop
|
||||||
|
Create (S, Word (I), Handles (I), R); pragma Assert (R = Ok);
|
||||||
|
end loop;
|
||||||
|
Create (S, 50, H, R); pragma Assert (R = Exhausted and H = 0);
|
||||||
|
for I in Handles'Range loop
|
||||||
|
Send (S, Handles (I), Word (I), Word (I * 10), R); pragma Assert (R = Ok);
|
||||||
|
end loop;
|
||||||
|
for I in Handles'Range loop
|
||||||
|
Receive (S, Handles (I), Word (I), M, R);
|
||||||
|
pragma Assert (R = Ok and M.Value = Word (I * 10));
|
||||||
|
Close (S, Handles (I), Word (I), R); pragma Assert (R = Ok);
|
||||||
|
end loop;
|
||||||
|
Ada.Text_IO.Put_Line ("ADA_PORTS_OK: FIFO, wrap, full/empty, grants, revocation, stale handles, exhaustion, port separation");
|
||||||
|
end Ports_Test;
|
||||||
Reference in new issue
Block a user