CuBit
1.0.0
Cubitos เป็นตัวประมวลผลแบบหลายโปรเซสเซอร์, 64 บิต, (บางส่วน) ระบบปฏิบัติการที่มีการตรวจสอบอย่างเป็นทางการ, วัตถุประสงค์ทั่วไปในปัจจุบันสำหรับสถาปัตยกรรม x86-64
Cubit ถูกเขียนขึ้นในภาษา Spark ของ ADA
Cubit เป็นงานที่กำลังดำเนินอยู่มาก! ต้องบอกว่าโปรดสปิน ยินดีต้อนรับผู้มีส่วนร่วม!
gprbuild , gnat ฯลฯ ใน $PATH ของคุณในการสร้าง bootable .iso คุณจะต้อง:
การพึ่งพา: คุณจะต้องใช้คอมไพเลอร์ GNAT 2020 และหากคุณต้องการสร้าง Live-CD คุณจะต้องใช้เครื่องมือ Xorriso และ Grub-Mkrescue และอาจเป็น GRUB-PC-BIN ขึ้นอยู่กับสภาพแวดล้อมของ Emulator/Virtualization ที่คุณใช้ สิ่งเหล่านี้อาจมีให้ในแพ็คเกจผู้จัดการแพ็คเกจของคุณ สิ่งนี้สามารถสร้างขึ้นใน Linux และบน Windows โดยใช้ WSL
git clone https://github.com/docandrew/CuBit.git
make
สิ่งนี้จะสร้าง Cubit และสร้างไฟล์ Live-CD .ISO ISO สามารถติดตั้งและทำงานใน VirtualBox, Bochs หรือ Qemu
| งาน | สั่งการ |
|---|---|
| สร้างเอกสาร (ใน build/docs) | make docs |
| ผู้ให้บริการ | make prove |
| สร้างเอกสาร HTML | make html |
ADA เป็นตัวพิมพ์ใหญ่ (ซึ่งเป็นสิ่งที่ดีตรงไปตรงมา) แต่มันทำให้สัญลักษณ์ที่ส่งออกทั้งหมดเป็นกรณีที่ต่ำกว่าดังนั้นทุกสิ่งในไฟล์. asm ที่อ้างอิงว่าสัญลักษณ์ต้องใช้เวอร์ชันที่ต่ำกว่าหรือระบุ external_name สำหรับสัญลักษณ์ในแง่มุม
ประเภทที่แจกแจงที่มี "หลุม" ทำให้ gnat ในการแทรกการตรวจสอบเวลารันไทม์สำหรับค่าที่ถูกต้องเมื่อกำหนดสิ่งเหล่านี้ ฉันไม่พบ pragma เพื่อปิดการตรวจสอบเหล่านี้ ในที่สุดเราจะเขียนฟังก์ชั่น Handler Exception ที่สามารถทำการตรวจสอบหรือทำให้เกิดความตื่นตระหนกของเคอร์เนล แต่สำหรับตอนนี้เติมค่าที่ชัดเจนเช่น bad_1, bad_2 ฯลฯ
โปรดตรวจสอบให้แน่ใจว่ามีการพิสูจน์ (โดยใช้ make prove ) ก่อนส่งคำขอดึง ระมัดระวังมากเกี่ยวกับคำอธิบายประกอบของ Pragma เพื่อปิดการใช้งานคำเตือน gnatprove จะให้คำเตือนปลอมเช่น statement has no effect หรือ unused assignment ซึ่งไม่ถูกต้องอย่างชัดเจน แต่โปรดตรวจสอบอีกครั้ง
บันทึกตัวแปรปรากฏขึ้นเพื่อแทรก cruft พิเศษบางส่วนในบันทึกพื้นฐานแม้ว่าจะใช้แพ็ค pragma ก็ตาม อย่าใช้สิ่งเหล่านี้เป็น "ซ้อนทับ" ที่ด้านบนของหน่วยความจำที่มีอยู่ตัวอย่างเช่นตาราง ACPI คุณจะมีปัญหาการจัดตำแหน่งกับบางฟิลด์และจบลงด้วยข้อมูลขยะ เช่นเดียวกันแม้กระทั่งสำหรับบันทึกที่ไม่แปรปรวนที่ใช้ discriminants
max_phys_alloc - ตั้งค่าใน config.ads นี่คือหน่วยความจำทางกายภาพสูงสุดที่ Cubit รองรับ มีข้อ จำกัด เพียงอย่างเดียวที่นี่เป็นจริงเนื่องจากการจัดสรร Boot Mem ได้รับการตั้งค่าเพื่อสร้างบิตแมปสำหรับหน่วยความจำทั้งหมดนี้ (128 GIB) ซึ่งใช้พื้นที่พอสมควร (เราอาจพิจารณาเพียงแค่จัดสรรส่วนกองที่ทำด้วยกันเชิงเส้นขนาดเล็กสำหรับการใช้เคอร์เนลและสร้างการจัดสรรที่ดีกว่าดังนั้นขีด จำกัด นี้ไม่ใช่ปัจจัยอีกต่อไป)
max_phys_address - หน่วยความจำทางกายภาพเชิง ทฤษฎี สูงสุดที่ฮาร์ดแวร์ของเรารองรับ (ถ้าเราใช้การแมปเชิงเส้น) ในกรณีของ x86-64 เรามีที่อยู่เสมือนจริง 48 บิตที่เป็นที่ยอมรับดังนั้นหากเราต้องการให้หน่วยความจำทางกายภาพทั้งหมดถูกแมปในหน่วยความจำเสมือนจริงเราจะเหลือประมาณ 280TB ซึ่งเราต้องแยกเพื่อใช้ในครึ่งสูงดังนั้น 128Tib โปรดทราบว่า Intel กำลังดูที่อยู่ 56 บิตด้วยตารางหน้าห้าระดับดังนั้นหมายเลขนี้อาจเปลี่ยนแปลงเร็ว ๆ นี้สำหรับ x86-64
max_phys_addressable - ที่อยู่หน่วยความจำทางกายภาพด้านบน ในระบบของเรา ที่เราตรวจพบเมื่อรันไทม์ เราพื้นที่หน่วยความจำแบบเส้นตรงถึงจุดนี้ (เริ่มต้นที่ 0xFFFF_8000_0000_0000)
max_phys_usable - ที่อยู่ RAM ที่ใช้งานได้ บนระบบของเรา อาจมีรูภายในสิ่งนี้ดังนั้นเราจึงไม่สามารถจัดสรรหน่วยความจำได้อย่างสุ่มสี่สุ่มห้าจากภายใต้ขีด จำกัด นี้ แต่คาดว่าจะมีการจัดสรรทางกายภาพที่จะจัดการกับที่อยู่จนถึงจุดนี้
โครงสร้างบางอย่างที่ใช้เช่นตาราง GDT และหน้าต้องตั้งค่าใน boot.asm ก่อนที่จะเปลี่ยนเป็นโหมดยาว สิ่งเหล่านี้เรียกว่าตาราง "bootstrap" GDT และหน้าตามลำดับ นอกจากนี้ยังมีการจัดสรรหน่วยความจำทางกายภาพ "บูต" ต่อมาเราได้แมปหน่วยความจำทางกายภาพทั้งหมดลงในครึ่งหนึ่งของเคอร์เนลพร้อมกับ GDT ใหม่ใน segment.adb สิ่งเหล่านี้เรียกว่า "ตารางเคอร์เนลหน้า" และ "เคอร์เนล GDT"
ตารางหน้า bootstrap identity-map เป็นหน่วยความจำ 1G แรกจากนั้นแมปอีกครั้งในครึ่งที่สูงขึ้นเริ่มต้นที่ 0xffff_8000_0000_0000 ดังนั้น P2V และ V2P (ทางกายภาพกับเสมือนจริง, เสมือนจริง) ทำงานโดยการเพิ่มและการลบอย่างง่ายเพราะคุณสามารถเข้าถึงหน่วยความจำทางกายภาพได้ที่ตัวอย่างเช่น 0x0000_0000_dead_beef ที่ที่อยู่เสมือนจริง 0x0000_0000_dead_beef
เมื่อเราเปลี่ยนไปใช้แผนที่เคอร์เนลเราไม่สามารถระบุหน่วยความจำได้อีกต่อไปโดยใช้ที่อยู่ทางกายภาพโดยตรง แต่จะต้องเข้าถึงที่อยู่ทางกายภาพเฉพาะโดยใช้ที่อยู่แมปเชิงเส้นที่ 0xFFFF_8000_0000_0000 เราเป็นเส้นตรงแผนที่หน่วยความจำทางกายภาพทั้งหมดใน 0xffff_8000_0000_0000 ถึง 0xffff_8fff_ffff_ffff
โปรดทราบว่าเนื่องจาก X86-64 ABI เคอร์เนลจะต้องเชื่อมโยงในหน่วยความจำ 2GIB บนสุดเมื่อใช้ MCMODEL = เคอร์เนล ดังนั้นตารางหน้าของเรายังต้องมีการแมปสำหรับ 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxxxxxxx
ใช่! ฉันพยายามทำให้รหัสเป็นมิตรกับผู้ที่ไม่คุ้นเคยกับ Cubitos, Ada หรือ Spark โปรดลองใช้ VM และแจ้งให้เราทราบว่าคุณคิดอย่างไร ข้อเสนอแนะเชิงลบและการวิจารณ์เชิงสร้างสรรค์ก็มีประโยชน์เช่นกัน
มันมีเอกสารหนักและยินดีต้อนรับผู้สนับสนุน!
Cubitos อาจเป็นจุดเริ่มต้นที่ดีสำหรับการวิจัยเชิงวิชาการ Spark มีฟักหลบหนีเพื่อทำการพิสูจน์ใน COQ ดังนั้นสำหรับผู้มีส่วนร่วมทางคณิตศาสตร์ที่ต้องการความท้าทายที่ดีดูสิ่งที่คุณสามารถพิสูจน์ได้เกี่ยวกับ cubitos!
Spark ใช้ Why3 Framework และ Z3 SMT Solver นักแก้ปัญหา SMT ที่ดีและรวดเร็วมักเป็นพื้นที่ที่น่าสนใจและศอกอาจเป็นวิธีที่ดีในการเปรียบเทียบพวกเขาสำหรับการใช้งานจริงอื่น ๆ
| องค์ประกอบรหัส | การประชุม |
|---|---|
| คำหลักของ ADA (พิมพ์, สำหรับ, ลูป, ฯลฯ ) | ตัวพิมพ์เล็กทั้งหมด |
| ประเภท (multibootstruct, pagetableentry ฯลฯ ) | อูฐที่เป็นตัวพิมพ์ใหญ่ |
| ชื่อแพ็คเกจ | อูฐที่เป็นตัวพิมพ์ใหญ่ |
| ตัวแปรฟังก์ชั่น (Kmain, tohexstring ฯลฯ ) | อูฐที่ไม่มีการสะสม |
| ค่าคงที่ (lt_gray, kern_base ฯลฯ ) | แคปทั้งหมด |
| ชื่อไฟล์ | ต่ำกว่าหรือ Snake_case ทั้งหมด |
หมายเหตุ: หากเชื่อมต่อกับส่วนประกอบภายนอกให้พูด Multiboot ชื่อตัวแปรควรใช้การประชุมเดียวกันกับ API ของส่วนประกอบนั้น ตัวอย่างเช่นโครงสร้างข้อมูลมัลติบูตมีฟิลด์เช่น mem_lower ฯลฯ
เราจะใช้ชื่อคำต่อคำเหล่านั้นที่นี่เพื่อความสะดวกในการอ้างอิงเอกสาร นี่ไม่ใช่กฎที่ยากและเร็ว หากชื่อ API นั้นมีความสับสนมากเกินไปสับสนใช้สัญกรณ์ฮังการีแปลก ๆ หรือเป็นใบ้ที่แบนออกมาแล้วอย่าลังเลที่จะเปลี่ยนชื่อพวกเขาในรหัส ADA
หลีกเลี่ยงตัวย่อที่ทวีคูณมากเกินไป คำทั่วไปเช่น "kern" สำหรับ "เคอร์เนล" หรือ "mem" สำหรับความทรงจำก็โอเคถ้าไม่มีความคลุมเครือ "VM" สำหรับหน่วยความจำเสมือนอาจสับสนกับ "เครื่องเสมือน" ดังนั้นจึงชอบ "Virtmem" หรือเพียงแค่สะกดออกมาอย่างสมบูรณ์ ควรใช้คำย่อเมื่อใช้กันอย่างแพร่หลายหรือการประชุมของฮาร์ดแวร์พื้นฐานเช่น ACPI
โปรดแปลงแท็บเป็น สี่ ช่องว่าง
การกระทำควรเป็นตอนจบสาย LF
หลีกเลี่ยงคำสั่ง "ใช้" เว้นแต่จำเป็นสำหรับผู้ประกอบการจากนั้น จำกัด การใช้งานของพวกเขาในโปรแกรมย่อยเฉพาะที่จำเป็นหรือใช้ประโยค "ใช้ประเภท" สิ่งนี้บังคับให้แพคเกจประเภทที่จะสะกดออกมาอย่างชัดเจนและเพื่อให้แพ็คเกจสามารถอ้างอิงได้อย่างง่ายดายและกระโดดไปยังในโปรแกรมแก้ไข ข้อยกเว้นสำหรับกฎนี้คือ:
ใช้คำว่า "เฟรม" เมื่ออ้างถึงหน่วยความจำทางกายภาพและ "หน้า" เมื่อพูดถึงหน่วยความจำเสมือน
โปรดใช้ชื่อเชิงพรรณนาสำหรับตัวแปรประเภท ฯลฯ เราไม่ขาดพื้นที่ฮาร์ดไดรฟ์ในการจัดเก็บซอร์สโค้ดดังนั้นใช้ชื่อที่ยาวขึ้น (ภายในเหตุผล) หากพวกเขาช่วยเสริมสร้างความเข้าใจรหัส
พยายามรักษาเส้นให้น้อยกว่า 80 ตัวอักษรเป็นส่วนใหญ่ แต่ถ้ามันส่งผลเสียต่อการอ่านเพื่อทำลายบรรทัดก็โอเคที่จะจับขีด จำกัด 80 ความกว้าง จุดสิ้นสุดของความคิดเห็นบรรทัดสามารถผ่านไปได้ 80 ถ้ามันเจ็บการไหลของรหัสเพื่อวางไว้ในบรรทัดของตัวเอง
หากโหมด Spark ถูกปิดใช้งานในร่างกายย่อยโปรดเพิ่มความคิดเห็นว่าทำไม นี่อาจใช้ได้อย่างสมบูรณ์แบบเช่น Inline ASM อย่างไรก็ตามลองและปรับโครงสร้างรหัสเพื่อเปิดใช้งานโหมด Spark - โดยเฉพาะข้อกำหนดย่อยโปรแกรมย่อย บางครั้งสิ่งนี้อาจเจ็บปวดเล็กน้อยเช่นการเปลี่ยนฟังก์ชั่นเป็นขั้นตอนด้วยพารามิเตอร์ "ออก" หลายตัว
ฉลองช่องว่าง ปล่อยให้รหัสหายใจ ใช้สองสายใหม่หลังจากแต่ละโปรแกรมย่อย หนึ่งบรรทัดใหม่หลังจากร่างกายย่อยมีความเหมาะสมหากโปรแกรมย่อยเป็นรูปแบบเล็กน้อยของกันและกันเช่นการโต้แย้งมากเกินไปและพวกเขาจะถูกจัดกลุ่มอย่างใกล้ชิดเพื่อชี้แจงความสัมพันธ์ของพวกเขา
ใช้ความคิดเห็นมากมายในรูปแบบ GNATDOC เห็นได้ชัดว่านี่เป็นพื้นที่ที่ความคิดเห็นแตกต่างกัน แต่ฉันเชื่อว่าการปฏิบัติต่อระบบปฏิบัติการเช่นห้องสมุดที่มีเอกสารอย่างละเอียดส่งเสริมความถูกต้องและทำให้เป็นมิตรกับผู้มีส่วนร่วมใหม่ นอกจากนี้ยังช่วยให้เอกสารที่สร้างใหม่โดยอัตโนมัติแทนที่จะเก็บเอกสารแยกต่างหาก เราทุกคนรู้ว่า API ที่ดีเมื่อเราเห็น
"แต่รหัสจะเปลี่ยนและความคิดเห็นจะล้าสมัย!"
ดังนั้น ... เอ่อ ... เพียงอัปเดตความคิดเห็น!
ยืมหน้าจากคู่มือผู้ให้บริการเครื่องบิน:
หมายเหตุ - หมายถึงข้อมูลที่ถือว่ามีความสำคัญในการเน้น
ข้อควรระวัง - หมายถึงข้อมูลที่อาจส่งผลให้ระบบล่มหรือการดำเนินการที่ไม่ถูกต้อง
คำเตือน - หมายถึงข้อมูลที่หากไม่ได้รับการพิจารณาอาจส่งผลให้สูญเสียข้อมูลผู้ใช้หรือความเสียหายต่อฮาร์ดแวร์พื้นฐาน
| คำที่ใช้ | ขนาด |
|---|---|
| ตอด | 4 บิต |
| ไบต์ | 8 บิต |
| คำ | 16 บิต |
| DWORD (คำสองคำ) | 32 บิต |
| Qword (quad-word) | 64 บิต |
สิ่งนี้รวมอยู่ที่นี่เพื่อหลีกเลี่ยงความสับสนที่ใช้เมื่ออธิบายอินเทอร์เฟซหรือส่วนประกอบฮาร์ดแวร์ที่ "คำ" อาจหมายถึงสิ่งอื่นนอกเหนือจาก 16 บิต เราหมายถึง 16 บิตในรหัสศอกเมื่อใช้ "คำ" ในความคิดเห็น ฯลฯ
โดยทั่วไปแล้วเราจะระบุความยาวของประเภทข้อมูลอย่างชัดเจนโดยใช้แพ็คเกจอินเตอร์เฟส ADA เช่น Unsigned_8, unsigned_32 ฯลฯ คำศัพท์ข้างต้นอาจใช้ในความคิดเห็นแทนที่จะสะกดคำว่า "ค่า 32 บิต"
ฟังก์ชั่น Spark ไม่ได้รับอนุญาตให้มีผลข้างเคียงใด ๆ หลายครั้งใช้ขั้นตอนแทนและจำเป็นต้องใช้พารามิเตอร์ OUT สำหรับผลลัพธ์แทนที่จะส่งคืนผลลัพธ์ มันค่อนข้างเจ็บปวดที่จะกำหนดชั่วคราวสำหรับผลลัพธ์ขั้นตอนทั้งหมด
คำจำกัดความของค่าคงที่ไม่สามารถใช้ร่วมกันได้ระหว่างรหัส ADA และไฟล์แอสเซมบลีดังนั้นบางส่วนจะทำซ้ำ ฉันพยายามที่จะรับค่าคงที่ทั้งหมดที่ใช้โดยไฟล์แอสเซมบลีใน Cubit.inc พร้อมกับบันทึกว่ามันอาจจะทำซ้ำในรหัส ADA โปรดตรวจสอบให้แน่ใจว่าหากคุณเปลี่ยนค่าใด ๆ เหล่านี้ว่าจะมีการเปลี่ยนแปลงในทั้งสองแห่ง หากคุณแนะนำค่าคงที่ของคุณเองที่ใช้ร่วมกันระหว่างแอสเซมบลีและรหัส ADA - ตรวจสอบให้แน่ใจว่าพวกเขาใช้ชื่อเดียวกัน!
Cubit แบ่งพื้นที่สแต็กแบบคงที่ออกเป็นชิ้นต่อ CPU ซึ่งแต่ละอันจะถูกแบ่งออกเป็นสแต็คหลักและรองสำหรับ CPU นั้น สแต็คหลักเติบโตขึ้นสแต็กรองเติบโตขึ้นมา ตัวชี้สแต็กหลักถูกตั้งค่าสำหรับ CPU หลักใน boot.asm และตั้งค่าสำหรับ CPU เพิ่มเติมแต่ละตัวเมื่อพวกเขาบูตใน boot_ap.asm
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 และ interrupts กระบวนการ 'เคอร์เนลสแต็คอาจถูกใช้งานซึ่งไม่มีสแต็ครอง
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.
| งาน | สั่งการ |
|---|---|
| สร้างเอกสาร (ใน build/docs) | make docs |
| ผู้ให้บริการ | make prove |
| สร้างเอกสาร HTML | make html |
คุณสามารถสร้างอิมเมจดิสก์ ext2 และอ่านเป็นศอกด้วยคำสั่งเหล่านี้แสดงที่นี่สำหรับดิสก์ 128MB:
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/ ที่คุณสามารถเพิ่มไฟล์ลงไปได้ยุ่งกับการอนุญาต ฯลฯ เมื่อคุณทำเสร็จแล้วให้ยกเลิกการเชื่อมต่อรูปภาพ โปรดทราบว่าการใช้งาน Ext2 ของ Cubit ในปัจจุบันรองรับขนาดบล็อก 4K เท่านั้น
umount vhd
ตอนนี้คุณมีอิมเมจดิสก์ที่คุณสามารถแปลงเป็นรูปแบบ VirtualBox ด้วย:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
คุณสามารถเพิ่มดิสก์ใหม่ภายใต้การจัดเก็บ -> ตัวควบคุม IDE ในการตั้งค่า VM ของคุณ คุณอาจต้องการใช้ชิปเซ็ต ICH6 Cubit ปัจจุบันใช้วิธี PIO โบราณสำหรับ ATA I/O หากคุณสร้างอิมเมจดิสก์และเพิ่มลงในคอนโทรลเลอร์ IDE ด้วยชิปเซ็ตที่แตกต่างกันการอ่านอาจล้มเหลว
โปรดทราบว่า Cubit เพิ่งอ่าน Ext2 SuperBlock ในปัจจุบัน แต่กำลังดำเนินการอยู่กับการสนับสนุนระบบไฟล์พื้นฐาน
โปรดทดลองใช้ RAM จำนวนหนึ่งจำนวน CPU ฯลฯ
VirtualBox เป็นเครื่องมือที่ดีสำหรับการทดสอบอย่างไรก็ตาม QEMU นั้นดีเมื่อคุณต้องการใช้ GDB เพื่อติดตามปัญหาบางอย่าง โปรดทราบว่า Cubit ใช้ประโยชน์จากคุณสมบัติ CPU ที่ค่อนข้างล่าสุดดังนั้นคุณจะต้องบอกให้ QEMU ใช้ชิปเซ็ตและ CPU ใหม่กว่า ตัวเลือก -machine q35 และ -cpu Broadwell ดูเหมือนจะทำงานได้ดี
คำสั่ง qemu w/o debugger:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
เคล็ดลับ GDB:
ลงทะเบียนข้อมูล add'l: rt Registers: rg64 Stack Trace: 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 (หมายเหตุ: ไม่ ".IS" ที่นี่เราต้องการไฟล์วัตถุเคอร์เนลเองซึ่งมีสัญลักษณ์ดีบั๊ก)
ในการเชื่อมต่อกับ QEMU: target remote localhost:1234 ใช้ (gdb) c เพื่อดำเนินการต่อ
จากที่นี่คำสั่ง GDB ปกติทำงานเช่น break , x , ฯลฯ
โปรดทราบว่า 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.
