CuBit
1.0.0
Cubitos는 현재 X86-64 아키텍처를위한 다중 프로세서, 64 비트 (부분적으로) 공식적으로 검증 된 일반 목적 운영 체제입니다.
Cubit은 Ada의 스파크 방언으로 작성되었습니다.
Cubit은 매우 진행중인 작업입니다! 그렇게 말하면서 스핀을주세요. 기고자 환영합니다!
gprbuild , gnat 등이있는 GNAT CE 2020 $PATH부팅 가능한 .iso를 만들려면 다음과 같은 것도 필요합니다.
종속성 : GNAT 2020 컴파일러가 필요하며 Live-CD를 구축하려면 Xorriso 및 Grub-Mkrescue 도구가 필요하며 어떤 에뮬레이터/가상화 환경에 따라 Grub-PC-Bin이 필요합니다. 이것들은 아마도 배포의 패키지 관리자에 제공 될 것입니다. 이것은 WSL을 사용하여 Linux와 Windows에서 구축 할 수 있습니다.
git clone https://github.com/docandrew/CuBit.git
make
큐빗을 구축하고 라이브 CD .iso 파일을 만듭니다. ISO는 VirtualBox, Boch 또는 QEMU에서 장착 및 실행할 수 있습니다.
| 일 | 명령 |
|---|---|
| 문서 작성 (빌드/문서) | make docs |
| 대리인을 달리십시오 | make prove |
| HTML 문서를 작성하십시오 | make html |
ADA는 대소 문자를 사용하지 않지만 (정직하고, 정직하게), 모든 내보내기 기호를 하위 신호하게 만들므로 기호가 하급 버전을 사용해야하거나 측면에서 기호에 대해 exteral_name을 지정하는 .AMS 파일의 모든 것을 만들어냅니다.
"구멍"을 포함하는 열거 된 유형은 GNAT가 할당 할 때 유효한 값에 대해 런타임 검사를 삽입하게합니다. 이러한 수표를 비활성화 할 프라그마를 찾을 수 없었습니다. 결국 우리는 검사를 수행하거나 커널 공황을 유발할 수있는 예외 핸들러 기능을 작성하지만 지금은 BAD_1, BAD_2 등과 같은 명백한 값으로 구멍을 채 웁니다.
풀 요청을 제출하기 전에 증거가 실행되도록하십시오 ( make prove ). 경고를 비활성화하기 위해 Pragma Annotate에 대해 매우주의하십시오. gnatprove statement has no effect 거나 unused assignment 와 같은 약간의 가짜 경고를 제공 할 것입니다. 그러나 이것을 다시 확인하십시오.
변형 레코드는 Pragma Pack을 사용하더라도 기본 레코드에 추가 cruft를 삽입하는 것으로 보입니다. 기존 메모리 (예 : ACPI 테이블) 위에 "오버레이"로 사용하지 마십시오. 일부 필드와 정렬 문제가 발생하고 정크 데이터로 끝납니다. 차별자를 사용하는 비 변수 기록에도 마찬가지입니다.
max_phys_alloc- config.ads에서 설정하면 Cubit가 지원하는 MAX 물리적 메모리입니다. Boot Mem allocator 가이 모든 메모리 (128 gib)에 대한 비트 맵을 생성하기 위해 설정되어 상당한 양의 공간을 차지하기 때문에 여기에는 제한이 있습니다. (우리는 커널 사용을위한 작은 선형 맵 힙 섹션을 따로 설정하고 더 나은 할당자를 구축 하므로이 한계가 더 이상 요인이되지 않습니다.)
max_phys_address- 하드웨어가 지원하는 최대 이론적 물리적 메모리 (선형 매핑을 사용하는 경우). X86-64의 경우 표준 48 비트 가상 주소가 있으므로 모든 물리적 메모리가 가상 메모리에 매핑되기를 원한다면 약 280TB를 남겨두고 있으며, 이는 128tib 더 높은 절반에 사용하기 위해 분할해야합니다. 인텔은 5 레벨 페이지 테이블로 56 비트 주소 지정을보고 있으므로이 숫자는 X86-64의 경우 곧 변경 될 수 있습니다.
max_phys_addressable- 런타임에서 감지하는 시스템의 상위 물리적 메모리 주소입니다. 이 시점까지 (0xffff_8000_0000_0000에서 시작).
max_phys_usable- 시스템의 상위 사용 가능한 RAM 주소입니다. 이 내부에는 구멍이있을 수 있으므로이 한계 아래에서 기억을 맹목적으로 할당 할 수는 없지만 물리적 할당자는이 시점까지 주소를 처리 할 것으로 예상됩니다.
GDT 및 페이지 테이블과 같은 일부 구조물은 Long 모드로 전환하기 전에 boot.asm 에 설정해야합니다. 이것을 각각 "부트 스트랩"GDT 및 페이지 테이블이라고합니다. "부팅"물리적 메모리 할당 자도 있습니다. 나중에, 우리는 물리적 메모리 전체를 segment.adb 의 새로운 gdt와 함께 커널의 더 높은 절반으로 다시 맵핑합니다. 이것들은 "커널 페이지 테이블"과 "커널 GDT"라고합니다.
부트 스트랩 페이지는 첫 번째 메모리의 첫 1g을 ID를 테이블 테이블 한 다음 0xffff_8000_0000_0000에서 시작하여 다시 절반으로 매핑합니다. 따라서 P2V 및 V2P (물리적-가상, 가상-물리적)는 간단한 추가 및 뺄셈을 통해 작동합니다. 예를 들어 0x0000_0000_DEAD_BEEF 0x0000_0000_DEAD_BEEF 및 0XFFFFF_8000_DEAD_BEEF에서 물리적 메모리에 액세스 할 수 있기 때문입니다.
커널 맵으로 전환하면 직접 물리적 주소를 사용하여 더 이상 메모리를 다룰 수 없습니다. 대신, 0xffff_8000_0000_0000의 선형 매핑 주소를 사용하여 특정 물리 주소에 액세스해야합니다. 우리는 0xffff_8000_0000_0000에서 0xffff_8fff_ffff_ffff의 모든 물리적 메모리를 선형 맵입니다.
X86-64 ABI로 인해 McModel = 커널을 사용할 때는 커널을 메모리의 상위 2Gib에 연결해야합니다. 따라서 당사 페이지 테이블에는 0xffff_ffff_8xxx_xxxx-> 0x0000_0000_0xxx_xxxx에 대한 매핑이 필요합니다.
예! 나는 Cubitos, Ada 또는 Spark에 익숙하지 않은 사람들에게 코드를 매우 친절하게 만들려고 노력했습니다. VM에서 시도해보고 당신의 생각을 알려주세요. 부정적인 피드백과 건설적인 비판도 유용합니다.
그것은 심하게 문서화되어 있으며 기고자들은 환영합니다!
Cubitos는 학업 연구를위한 좋은 출발점 일 수 있습니다. Spark는 COQ에서 증거를 수행하기위한 탈출 해치를 가지고 있으므로 좋은 도전을 원하는 수학적으로 기고자들에게 Cubitos에 대해 증명할 수있는 것을보십시오!
Spark는 Why3 프레임 워크 및 Z3 SMT 솔버를 사용합니다. 좋고 빠른 SMT 솔버는 항상 관심있는 영역이며 Cubitos는 다른 실제 용도로이를 벤치마킹하는 좋은 방법 일 수 있습니다.
| 코드 요소 | 협약 |
|---|---|
| ADA 키워드 (유형, for, 루프 등) | 모든 소문자 |
| 유형 (Multibootstruct, pagetableentry 등) | 자본화 된 낙타 |
| 패키지 이름 | 자본화 된 낙타 |
| 변수, 기능 (Kmain, Tohexstring 등) | 캡시되지 않은 낙타 |
| 상수 (lt_gray, kern_base 등) | 모든 캡 |
| 파일 이름 | 모든 낮은 또는 snake_case |
참고 : 외부 구성 요소에 인터페이스하는 경우 Multiboot를 말하면 변수 이름은 해당 구성 요소의 API와 동일한 규칙을 사용해야합니다. 예를 들어, Multiboot Info Struct에는 MEM_LOWER와 같은 필드가 있습니다.
문서화의 용이성 참조를 위해 여기에서 해당 이름을 verbatim을 사용할 것입니다. 이것은 어려운 규칙이 아닙니다. API 이름이 지나치게 혼란 스럽거나 혼란 스러우거나 이상한 헝가리 표기법을 사용하거나 멍청한 멍청한 경우 ADA 코드에서 자유롭게 이름을 바꾸십시오.
지나치게 약어를 피하십시오. "커널"에 대한 "kern"또는 메모리의 "mem"과 같은 일반적인 용어는 모호함이 없으면 괜찮습니다. 가상 메모리의 "VM"은 "Virtual Machine"과 혼동 될 수 있으므로 "Virtmem"을 선호하거나 철자를 완전히 철자하십시오. 약어는 널리 사용되거나 ACPI와 같은 기본 하드웨어의 협약 인 경우에만 사용해야합니다.
탭을 4 개의 공간으로 변환하십시오.
커밋은 LF 라인 엔딩이어야합니다.
운영자에게 달리 필요하지 않는 한 조항을 "사용"한 다음 필요한 경우 특정 서브 프로그램으로 사용하거나 "사용 유형"조항을 사용하십시오. 이로 인해 유형의 패키지가 명시 적으로 철자를 낼 수 있으므로 패키지를 편집기에서 쉽게 참조하고 점프 할 수 있습니다. 이 규칙에 대한 예외는 다음과 같습니다.
물리적 메모리를 참조 할 때 "프레임"이라는 용어를 사용하고 가상 메모리를 논의 할 때 "페이지"를 사용하십시오.
변수, 유형 등에 대한 설명 이름을 사용하십시오. 소스 코드를 저장할 하드 드라이브 공간이 부족하지 않으므로 코드에 대한 이해를 키우는 데 도움이되면 더 긴 이름 (이유 내에서)을 사용하십시오.
선을 80 chars 미만으로 유지하려고 노력하지만 선을 깨뜨리는 가독성에 부정적인 영향을 미치면 80 층의 한계를 파열해도 괜찮습니다. 코드의 흐름이 자신의 라인에 놓기 위해 코드의 흐름에 해를 끼치면 80을 넘어갈 수 있습니다.
하위 프로그램 본문에서 Spark Mode가 비활성화 된 경우 의견을 추가하십시오. 이것은 완벽하게 유효 할 수 있습니다, 즉 인라인 ASM. 그러나 코드를 시도하고 재구성하여 Spark 모드, 특히 하위 프로그램 사양을 활성화하십시오. 때때로 이것은 약간 고통스럽고, 즉 여러 "out"매개 변수가있는 절차에 대한 기능을 변화시킬 수 있습니다.
공백을 축하하십시오. 코드가 숨을 쉬게하십시오. 각 하위 프로그램 후에 두 개의 최신 라인을 사용하십시오. 하위 프로그램이 서로의 작은 변형, 즉 과부하 된 인수 인 경우 하위 프로그램 본문의 새로운 라인이 적절하며 관계를 명확히하기 위해 밀접하게 그룹화됩니다.
GNATDOC 형식으로 많은 주석을 사용하십시오. 이것은 분명히 의견이 다른 영역이지만, 철저한 문서로 도서관처럼 OS를 취급하면 정확성을 장려하고 새로운 기고자에게 더 친숙합니다. 이를 통해 문서를 개별적으로 유지하기보다는 자동 생성 문서화가 더 쉬워집니다. 우리는 우리가 하나를 볼 때 좋은 API를 알고 있습니다.
"그러나 코드는 변경되고 의견이 오래되지 않을 것입니다!"
그래서 ... 어 ... 댓글을 업데이트하십시오!
항공기 운영자 매뉴얼에서 페이지를 빌리기 :
참고 - 강조해야 할 중요한 정보를 나타냅니다.
주의 - 고려되지 않은 경우 시스템 충돌 또는 잘못된 작업이 발생할 수있는 정보를 나타냅니다.
경고 - 고려되지 않은 경우 사용자 데이터 손실 또는 기본 하드웨어 손상을 초래할 수있는 정보를 나타냅니다.
| 사용 된 용어 | 크기 |
|---|---|
| 조금씩 깨물다 | 4 비트 |
| 바이트 | 8 비트 |
| 단어 | 16 비트 |
| dword (이중 단어) | 32 비트 |
| Qword (쿼드 단어) | 64 비트 |
이것은 "Word"가 16 비트 이외의 것을 의미 할 수있는 인터페이스 또는 하드웨어 구성 요소를 설명 할 때 사용되는 혼란을 피하기 위해 여기에 포함됩니다. 댓글 등에 "Word"를 사용할 때 항상 큐빗 코드에서 16 비트를 의미합니다.
일반적으로 ADA 인터페이스 패키지 (예 : Unsigned_8, Unsigned_32 등)를 사용하여 데이터 유형의 길이를 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 명시 적으로 설명합니다. 예를 들어 위의 용어는 "32 비트 값"을 철자하지 않고 주석에 사용될 수 있습니다.
Spark 함수는 부작용이 없을 수 없으므로 여러 번 절차가 대신 사용되며 결과를 반환하는 것보다 결과에 대한 OUT 매개 변수가 필요합니다. 모든 절차 결과에 대해 임시를 할당하는 것은 약간 고통 스럽습니다.
상수의 정의는 ADA 코드와 어셈블리 파일간에 (쉽게) 공유 할 수 없으므로 일부는 복제됩니다. ADA 코드에서 복제 될 수있는 위치와 함께 Cubit.inc의 어셈블리 파일에서 사용하는 모든 상수를 얻으려고 노력했습니다. 이 값 중 하나를 변경하면 두 곳에서 변경되어 있는지 확인하십시오. 어셈블리와 ADA 코드간에 공유되는 자신의 상수를 소개하는 경우 동일한 이름을 사용해야합니다!
Cubit은 정적 스택 영역을 CPU 덩어리로 나눕니다. 각각은 해당 CPU의 1 차 및 2 차 스택으로 분할됩니다. 1 차 스택이 자라면서 보조 스택이 자랍니다. 기본 스택 포인터는 boot.asm의 기본 CPU에 대해 설정되며 Boot_ap.asm에서 부팅 할 때 각 추가 CPU에 대해 설정합니다.
STACK_TOP +-----------------------+
| |
| CPU 0 Primary Stack |
| |
+-----------------------+
| CPU 0 Secondary Stack |
+-----------------------+
| |
| CPU 1 Primary Stack |
| |
+-----------------------+
| CPU 1 Secondary Stack |
+-----------------------+
| . |
| . |
| . |
+-----------------------+
| |
| CPU N Primary Stack |
| |
+-----------------------+
| CPU N Secondary Stack |
STACK_BOTTOM +-----------------------+
보조 스택 ss_init 호출은 각 CPU 부팅 중에 이루어집니다. 보조 스택 오버 플로우는 런타임에 감지해야하지만주의를 기울여야합니다. SYSCALLS 및 인터럽트 중에 프로세스 '커널 스택이 사용 중일 수 있으며, 이는 보조 스택이 없습니다.
X 완료를 의미합니다- 진행중인 것을 의미합니다 [ ] There are a lot of potential circular dependencies for just "proof stuff",
i.e. preconditions where we don't want to call a blockingSleep until
interrupts are enabled -> don't want to enable interrupts until the
interrupt vector is loaded -> interrupt vector will update the value that
blockingSleep depends on. It might make sense to keep a big "state"
.ads file with nothing but Ghost variables used in SPARK proofs. It would
not have any dependencies itself, but could be included by everything else
to update their states. Downside is that it might grow huge and unwieldy,
and sorta breaks encapsulation. Might make proofs take a long time too.
[X] Put the stack at a more sensible location
[X] Per-CPU Stacks
[X] Secondary Stacks
[X] Print out full register dump with exceptions
[-] Make type-safe more of the address/number conversions I'm doing.
[-] Error-handling. Need to formalize the mechanism, could get very messy with MP.
[X] Exceptions (Last chance handler)
[ ] Broadcast panic to other CPUs
[ ] Figure out a keyboard scancode -> key array scheme with a future eye towards
internationalization. Maybe just use SDL's keyboard handling scheme and let them sort it out.
[X] Physical memory allocator
[X] Boot-mem allocator using bitmaps
[X] Boot phys memory allocator
[X] Keep track of free space as we allocate/free
[X] Buddy allocator
[X] Virtual memory mapper
[X] Mark 0 page as not present
[X] Re-map kernel pages with appropriate NXE bits, etc. depending on region.
[-] Virtual memory allocator
[-] Demand paging.
[-] Processes / Threads
[ ] Kernel Tasks
[X] Usermode
[-] Scheduler
[ ] Implement killing processes.
[ ] Suspend
[ ] Sleep / Wakeup
[-] ACPI tables
[X] Find RSDT/XSDT
[X] Sane code for parsing these.
[-] APIC
[ ] HPET
[ ] MCFG - PCI express
[ ] SSDT?
[-] I/O APIC
[-] Multiprocessing
[ ] MP Tables (necessary?)
[-] LAPIC
[ ] X2APIC
[ ] Hardware
[X] MSRs
[-] Full CPUID detection
[-] Disk drivers
[ ] MBR/GPT Partition Table
[-] PCI bus
[-] Hard Drives
[-] ATA
[-] AHCI
[ ] PCI express
[ ] Enhanced Configuration Access Mechanism (ECAM) via MCFG tables
[ ] NVMe
[ ] Sound
[ ] Video Drivers
[-] VESA Modes
[-] Filesystem / VFS Layer
[ ] Develop FS-agnostic set of VFS hooks to syscalls
[ ] Develop Drive-agnostic set of VFS hooks to hardware
[-] Ext2
[ ] Networking
[ ] Interface driver
[ ] TCP/IP Stack - RecordFlux should help here.
[ ] Security
[ ] ASLR / KASLR
[ ] Disable certain branch speculation behavior (see x86.MSR)
[ ] if processor supports IBRS in ARCH_CAPABILITIES
[-] KPTI
[ ] Disable KPTI if ARCH_CAPABILITIES MSR indicates not susceptible to RDCL
[ ] Sensible Kernel-Mode-Setting / Framebuffer / Compositor arrangement
[ ] Wow Factor / Eye Candy
[ ] Sweet GRUB splash screen w/ logo
[-] Syscalls
[X] SYSCALL/SYSRET working
[ ] Microkernel Concepts?
[ ] User-mode drivers?
[ ] IPC?
[-] More formal proofs of kernel correctness
[ ] Preventing race conditions - may not be feasible outside of
Ravenscar profile, which doesn't really apply to us.
[-] Implement more of the Ada standard library, especially for Tasks.
[-] Init model - should this look like UNIX? Something else?
[ ] Security Model
[-] Codify it
[ ] Prove it
[ ] Implement it
[-] IMGUI framework
[-] Make all package names Uppercase
[-] Rename all setupXYZ to just setup, since package name is already there.
[X] New Makefile
[-] Use gnatdoc format in comments
[ ] Edit gnatdoc format so NOTE, CAUTION, WARNING shows up as different
colors.
[ ] Edit gnatdoc format to ignore the leading and trailing horizontal rules
[-] Work out a CI/CD pipeline
[ ] Proof Step
[ ] Unit Testing
[X] Build
[ ] Integration/Functional Testing
[X] Generate Documentation
[-] Build installers, isos, etc.
[ ] Write unit tests
[ ] Fuzzing
[ ] Integration tests that run in the OS.
| 일 | 명령 |
|---|---|
| 문서 작성 (빌드/문서) | make docs |
| 대리인을 달리십시오 | make prove |
| HTML 문서를 작성하십시오 | make html |
Ext2 디스크 이미지를 만들고 128MB 디스크에 표시된이 명령으로 Cubit에서 읽을 수 있습니다.
dd if=/dev/zero of=vhd.img bs=1M count=128
mkfs -t ext2 -b 4096 vhd.img
mkdir vhd
mount -t auto -o loop vhd.img vhd
이제 vhd/ 에 빈 파일 시스템이있어 파일을 추가하고 권한을 부드럽게 만들 수 있습니다. 완료되면 이미지를 마운다. Cubit의 Ext2 구현은 현재 4K 블록 크기 만 지원합니다.
umount vhd
이제 다음과 같이 가상 박스 형식으로 변환 할 수있는 디스크 이미지가 있습니다.
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
VM 설정에서 스토리지 -> IDE 컨트롤러에서 새 디스크를 추가 할 수 있습니다. ICH6 칩셋을 사용하고 싶을 것입니다. Cubit은 현재 ATA I/O에 고대 PIO 방법을 사용합니다. 디스크 이미지를 만들어 다른 칩셋으로 IDE 컨트롤러에 추가하면 읽기가 실패 할 수 있습니다.
Cubit은 현재 EXT2 슈퍼 블록을 읽지 만 기본 파일 시스템 지원으로 진행되고 있습니다.
다른 양의 RAM, CPU 수 등을 실험하십시오.
VirtualBox는 테스트하기에 좋은 도구이지만 QEMU는 GDB를 사용하여 특정 문제를 추적해야 할 때 좋습니다. Cubit은 상당히 최근의 CPU 기능을 사용하므로 QEMU에게 최신 칩셋과 CPU를 사용하도록 지시해야합니다. -machine q35 및 -cpu Broadwell 옵션이 잘 작동하는 것 같습니다.
디버거가없는 QEMU 명령 :
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
GDB 팁 :
추가 추가 정보 : rt 레지스터 : rg64 스택 추적 : k
QEMU를 사용하여 디버그를 사용하려면 :
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
QEMU는 디버거를 기다리는 동안 일시 정지 상태로 시작합니다.
그런 다음 gdb : gdb cubit_kernel 실행합니다 (참고 : no ".iso"여기서는 디버깅 기호가 포함 된 커널 객체 파일 자체를 원합니다).
QEMU에 연결하려면 : target remote localhost:1234 사용 (gdb) c 대상으로합니다. c.
여기에서 break , x 등과 같은 일반 GDB 명령이 작동합니다.
Hyper-V는 현재 .iso를 부팅하는 것처럼 보이지 않습니다. 다른 가상화 또는 에뮬레이션 플랫폼이 권장됩니다.
git clone https://github.com/Componolit/RecordFlux
install >= Python 3.6
install pip
install virtualenv if Python 3 not the default
source bin/activate
python setup.py build
python setup.py install
Now the rflx script at bin/rflx should work.
