البناء
التشغيل على Raspberry Pi 5
ما تشتريه، وكيف تبني بطاقة SD وتكتبها، وكيف تقرأ السجل التسلسلي للوحة وتفحصه، وكيف تشغّل الأنظمة على Pi 5 دون إشراف أو تشاهد واجهة المستخدم على شاشة HDMI الخاصة به.
Raspberry Pi 5 هي اللوحة المرجعية لـ NoWayOS: منخفضة التكلفة، ومتوفرة على نطاق واسع، وهي اللوحة التي تجري عليها أولى اختباراته على العتاد. والنظام الذي ينجح في QEMU يُفحص على Pi مقابل ملف التوقعات نفسه، من السجل التسلسلي للوحة.
قاعدتان للوحة. لا تصل أبدًا محوّلًا تسلسليًا بجهد 5 V بمنفذ UART في Pi: فهو منفذ 3.3 V. ولا تبرمج أبدًا ذاكرة Pi القابلة للبرمجة مرة واحدة، ولا تفعّل الإقلاع الآمن على لوحة تطوير: فكلاهما لا رجعة فيه. ويرفض
make sdcardأي ملفconfig.txtقد يفعل أيًّا منهما، أو يغيّر جهد اللوحة.
ما تحتاجه
| العنصر | ملاحظات |
|---|---|
| Raspberry Pi 5 | طُوِّر واختُبر على لوحة 16 GB. كل أمر يسمّي اللوحة rpi5b_2gb: وهو إعداد seL4 الخاص بـ Pi 5 الذي يستخدم أول 2 GB من ذاكرتها، ويمنح البناء seL4 منها أقل بقليل من 1 GB. لذا يُفترض ألا تحتاج لوحات 2 و 4 و 8 GB إلى أي شيء مختلف، لكنها لم تُجرَّب |
| مزوّد الطاقة | المزوّد الرسمي بجهد 5 V وتيار 5 A عبر USB-C، أو مزوّد بالجودة نفسها. فـ Pi 5 الذي لا يحصل على طاقة كافية يتصرف تصرفًا غريبًا كأنه خلل برمجي |
| بطاقة microSD | لقسم الإقلاع الذي يبنيه make sdcard |
| Raspberry Pi Debug Probe | يناسب كابل UART الخاص به موصل التصحيح ثلاثي الأطراف في Pi 5. ويعمل أيضًا أي محوّل من USB إلى تسلسلي بجهد 3.3 V مع الكابل المناسب |
| شاشة HDMI، ولوحة مفاتيح وفأرة USB | لواجهة المستخدم. صِل الشاشة قبل التشغيل: فالبرنامج الثابت لا يهيئ الشاشة إلا عند الإقلاع. تعمل لوحات المفاتيح والفئران من فئة USB boot؛ أما الموزعات فلا تعمل بعد |
ابنِ بطاقة SD
make sdcard BOARD=rpi5b_2gb SYSTEM=hello
يكتب هذا قسم الإقلاع للبطاقة في build/rpi5b_2gb/hello/sdcard/: U-Boot، وشجرة الأجهزة وتراكباتها، و config.txt، وصورة seL4 loader.img، وملفات التراخيص، وملف SHA256SUMS لفحص البطاقة بعد ذلك. ويُبنى U-Boot من المصدر داخل الحاوية، بطريقة قابلة لإعادة الإنتاج.
اكتب البطاقة
على macOS
- اعثر على البطاقة بالأمر
diskutil list: فهي external, physical، وبحجم البطاقة. الخطوة التالية تمحو ذلك القرص بالكامل، فتحقق من الرقم مرتين. - هيّئها، باسم
PIBOOT:
diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN
- انسخ الملفات، وتحقق من وصول كل منها سليمًا (لا يطبع هذا شيئًا حين تتطابق كلها):
cp -RX build/rpi5b_2gb/hello/sdcard/ /Volumes/PIBOOT/
dot_clean -m /Volumes/PIBOOT
(cd /Volumes/PIBOOT && shasum -a 256 -c SHA256SUMS | grep -v ': OK$')
- أخرجها بالأمر
diskutil eject /dev/diskN، وضعها في Pi.
على Linux
الخطوات نفسها بأدوات Linux (بطاقات المشروع نفسه تُصنع على macOS):
- اعثر على البطاقة بالأمر
lsblk -p: قرص بحجم البطاقة، مثل/dev/sdXأو/dev/mmcblk0. الخطوة التالية تمحو ذلك القرص بالكامل، فتحقق من الاسم مرتين، وألغِ تركيب أي من أقسامه. - أنشئ عليها قسمًا واحدًا بنظام FAT32، باسم
PIBOOT(مع تثبيتdosfstoolsوparted):
sudo parted --script /dev/sdX mklabel msdos mkpart primary fat32 1MiB 100% set 1 lba on
sudo mkfs.vfat -F 32 -n PIBOOT /dev/sdX1
- انسخ الملفات، وتحقق من وصول كل منها سليمًا (لا يطبع هذا شيئًا حين تتطابق كلها):
sudo mount /dev/sdX1 /mnt
sudo cp -r build/rpi5b_2gb/hello/sdcard/. /mnt/
(cd /mnt && sha256sum -c SHA256SUMS | grep -v ': OK$')
sudo umount /mnt
- ضعها في Pi.
صِل وحدة التحكم التسلسلية
صِل Debug Probe بـ موصل التصحيح المخصص ثلاثي الأطراف في Pi 5، بين منفذَي HDMI، لا بأطراف GPIO. ويعمل بسرعة 115200 baud، 8N1. ويظهر المسبار على Mac باسم /dev/cu.usbmodem…، وعلى Linux باسم /dev/ttyACM0 أو ما شابه (يجب أن يكون مستخدمك ضمن المجموعة dialout).
ابدأ الالتقاط قبل تشغيل Pi، إقلاع واحد لكل سجل:
mkdir -p build/rpi5b_2gb/hello
(stty 115200 raw -echo; cat) < /dev/cu.usbmodemXXXX | tee build/rpi5b_2gb/hello/serial.log
أبقِ الإعدادات والقراءة في أمر واحد، كما هنا: ففي macOS يعود الفتح الثاني للمنفذ إلى سرعة 9600 baud. وعلى Linux، اضبط المنفذ بالأمر stty -F /dev/ttyACM0 115200 raw -echo واقرأه بالأمر cat /dev/ttyACM0. وأوقف الالتقاط بـ Ctrl-C بعد آخر سطر متوقع.
عند التشغيل، يعدّ U-Boot تنازليًا ثلاث ثوانٍ ثم يُقلع loader.img من البطاقة. ولتتوقف عند موجّه الأوامر الخاص به بدلًا من ذلك، اكتب stopboot أثناء العد التنازلي. (لا توقفه إلا هذه الكلمة، فلا يمكن للضجيج الذي يلتقطه خط تسلسلي غير موصول أن يُبقي الجهاز عالقًا عند U-Boot.)
افحص السجل
افحص سجل اللوحة مقابل ملف التوقعات الخاص بالنظام، بالقواعد نفسها التي تُفحص بها مخرجات QEMU:
make check-serial SYSTEM=hello LOG=build/rpi5b_2gb/hello/serial.log
أضف BOARD=rpi5b_2gb للنظام الذي له ملف توقعات خاص به لـ Pi.
شغّل الأنظمة دون إشراف
مع توصيل المسبار، يشغّل make pi-run سلسلة من الأنظمة على اللوحة دون نقل أي بطاقة ودون وجود أحد عند اللوحة. شغّله على جهازك نفسه، لا داخل الحاوية (ففي Mac، لا ترى آلة Podman الافتراضية أجهزة USB التسلسلية). ويحتاج هناك إلى Python 3.11 أو أحدث، مع المكتبة القياسية فقط:
make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS="hello ipc-demo isolation-test"
لكل نظام، يبني الصورة في الحاوية، ويعيد تعيين اللوحة، ويرسل الصورة عبر الخط التسلسلي ويتحقق من وصولها سليمة، ويفعّل مؤقت المراقبة في اللوحة، ثم يشغّلها. ويُفحص كل سجل فور وصوله، ويعيد مؤقت المراقبة تعيين اللوحة للنظام التالي. وكل أمر يكتبه يُعاد صداه ويُفحص قبل إدخاله. وتُحفظ السجلات في build/rpi5b_2gb/pi-run/.
شاهد واجهة المستخدم
مع توصيل الشاشة قبل التشغيل:
make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS=ui-demo PI_WATCHDOG=15
يشغّل هذا الأمر الجلسة المُعدّة مسبقًا لواجهة المستخدم على شاشة HDMI ويفحص قيمة التجزئة لكل إطار. ولترك نظام يعمل كي يشاهده شخص ما، دون مؤقت مراقبة، استخدم make pi-show PI_DEVICE=… SYSTEM=ui-demo؛ ويظل يعمل حتى يُقطع التيار عن اللوحة ثم يُعاد.
حين يفشل شيء ما
عد إلى آخر صورة نجحت، وافحص الخط التسلسلي وسلسلة الإقلاع مجددًا، قبل أن تغيّر أكثر من شيء واحد في كل مرة. وإذا لم يظهر شيء على الإطلاق قبل U-Boot، فافحص إعداد BOOT_UART في محمّل الإقلاع و enable_uart=1 في ملف config.txt على البطاقة قبل أن تشك في المسبار أو التوصيلات.