Readme

You can find more about the Pip protokernel at its website.

The source code is covered by CeCILL-A licence.

The Pip Development Team:

• Damien Amara
• Nicolas Dejon
• Gilles Grimaud
• Michaël Hauspie
• Samuel Hym
• David Nowak
• Claire Soyez-Martin
• Florian Vanhems

Past members of the Pip Development Team:

• Quentin Bergougnoux
• Julien Cartigny
• Étienne Helluy Lafont
• Narjes Jomaa
• Paolo Torrini
• Mahieddine Yaker

Getting started

You can generate the "Getting Started" tutorial by invoking make gettingstarted. The full documentation is generated by invoking make doc.

Dependencies

Pip is known to build correctly with this toolchain:

• COQ Proof Assistant version 8.13.1
• Doxygen version 1.8.13 and above (for documentation generation)
• GCC version 8.3.0 and above
• GDB version 8.2.1 and above
• GNU Make version 4.3 and above
• grub-mkrescue (for ISO image generation; unnecessary for i386 target though)
• haskell-stack version 1.7.1 and above (is a cross-platform program for developing Haskell projects)
• NASM version 2.14 and above
• QEMU i386 version 3.1.0 and above
• Texlive any version or another latex tools

Building the Pip

You can pass several arguments to make to compile the Pip.

• all: Build target
• proofs: Proofs target
• qemu-elf | qemu-iso: QEMU targets
• doc | doc-c | doc-coq | gettingstarted: Documentation targets
• toolchain.mk: Configure script target
• clean | realclean: Clean targets

Building partitions

Each partition is located into src/arch/{architecture}/partitions/{partition}

• Configure the toolchain by copying src/partitions/{architecture}/toolchain.mk.template to src/partitions/{architecture}/toolchain.mk, then edit the latter to your needs.
• You can use the minimal partition as a base to develop more elaborated software.
• You can compile the partition by invoking make in the partition's directory.

Kernel structure

The kernel is divided into three parts.

• MAL: The Memory Abstraction Layer is used to provide small functions to manipulate the MMU
• Core: The logic of Pip
• Boot: The bootstrap code that initializes required hardware and then boots Pip

Source code structure

• _CoqProject is a mandatory configuration file for Coq.
• src/ contains the source base directory.
• src/core contains the Pip source folder.
• src/extraction contains the code to extract Coq services.
• src/interface contains the interface between Coq and C.
• src/model contains the Coq code.
• src/arch/x86_multiboot/MAL contains the Memory Abstraction Layer source.
• src/arch/x86_multiboot/boot contains the "cbits", i.e the required C and assembly code required to boot the coq kernel.
• src/arch/x86_multiboot/partitions contains the top-level partitions.
• tools/ contains some scripts and tools that may be useful.
• proof/ contains the Coq proof.

Serial configuration

Pip can already boot on real hardware. If available, the first serial output (COM1) should be used for debugging output.

The required configuration is 38400 bauds, 8 bits, no parity, one stop bit. You can also enable automatic line feed and carriage return in Minicom (2.7+) for user-friendly output.

Compiling on Linux

The compilation on Linux should be as easy as to install the i386-elf toolchain as well as the other requirements, and use the Makefile to generate a binary image.

Use your favourite package manager to install Coq, Doxygen, GCC, GDB, GNU Make, GRUB, haskell-stack, NASM, QEMU and Texlive.