시작하기

NoWayOS는 버전이 고정된 개발 컨테이너 하나 안에서 빌드되므로, 여러분의 컴퓨터에 따로 갖출 것은 거의 없습니다. 이 페이지에서는 아무것도 없는 상태에서 데모를 실행하기까지 안내합니다. 다음 페이지에서는 QEMU에서 실제 seL4 시스템을 부팅하고, 그다음 페이지에서는 이를 Raspberry Pi 5에 올립니다.

필요한 것

• Podman과 GNU Make. Docker도 됩니다. 각 make 명령에 ENGINE=docker를 덧붙이십시오.
• 저장소를 클론할 git.
• 컴퓨터에 Rust도 seL4 도구도 필요 없습니다. Rust 툴체인, Microkit SDK, QEMU는 모두 정확한 버전으로 고정되어 개발 컨테이너 안에 들어 있습니다.

macOS에서 Podman은 가상 머신 안에서 컨테이너를 실행합니다. CPU 몇 개와 메모리 몇 기가바이트를 주어 가상 머신을 한 번 만들고 시작하십시오. 예를 들면 다음과 같습니다.

podman machine init --cpus 4 --memory 8192
podman machine start

NoWayOS는 Apple 실리콘(arm64)에서 개발됩니다. x86-64에서도 개발 이미지의 패키지 버전은 고정되고 검토되었지만, 그곳에서 이미지를 처음부터 끝까지 빌드하고 테스트해 보지는 아직 않았습니다.

NoWayOS 전용 폴더 만들기

개발 컨테이너는 클론한 저장소의 한 단계 위 폴더를 마운트합니다. 나란히 클론한 저장소끼리 서로를 참조해 빌드할 수 있도록 하기 위해서입니다. 먼저 저장소들을 담을 폴더를 만드십시오.

mkdir nowayos-work && cd nowayos-work
git clone https://github.com/NoWayOS/nowayos.git
cd nowayos

개발 컨테이너 빌드하기

make container

버전이 고정된 개발 이미지를 빌드합니다. Rust 툴체인, Microkit SDK, QEMU, 검사 도구가 들어 있습니다. 첫 빌드는 몇 분 걸리며(Apple 실리콘 Mac에서는 4분 미만), 약 4.7 GB 크기의 이미지가 만들어집니다. tools/container/Containerfile이 바뀔 때마다 다시 실행하십시오. 다른 모든 타깃은 오래된 이미지에서는 실행을 거부하고 그 사실을 알려 줍니다.

데모 실행하기

make demo

데모는 탭, 클릭, 키 입력으로 이루어진 스크립트 세션을 갖춘 작은 양식 애플리케이션입니다. seL4도 QEMU도 없이 호스트 시뮬레이션으로 실행되며, 단계마다 NoWayOS의 실제 UI 코어와 렌더러로 프레임을 그립니다. 각 프레임은 승인된 이미지와 비교되며, 실행은 다음과 같이 끝납니다.

demo: PASS - … steps, every frame as approved

어느 프레임이든 단 한 픽셀이라도 다르면, 어느 단계인지 알려 주고 실패합니다.

둘러보기

make # every target, with a line on each
make test # unit, property, doc and golden-image tests
make lint # rustfmt, then clippy with warnings as errors

모든 타깃은 개발 컨테이너에서 실행되며, 컨테이너도 알아서 시작합니다. 저장소의 DEVELOPING.md에 코드 구조와 함께 모든 타깃이 나열되어 있습니다.

문제가 생기면

• error: … was not built from the current … Containerfile: 컨테이너를 빌드한 뒤로 컨테이너 정의가 바뀌었습니다. 메시지대로 make container를 다시 실행하십시오.
• Podman에 연결할 수 없음: macOS에서는 podman machine start로 가상 머신을 시작하십시오.
• 빌드 중 메모리 부족: Podman 가상 머신에 메모리를 더 주십시오. 전체 관문인 make ci는 데모보다 훨씬 많은 메모리가 필요한 모델 검사 증명을 실행합니다(검사와 증거).