Build failing - initramfs too large

[Sven Anderson]

Hi,

first of all, thanks for that great work and project!

I'm trying to build the demo image with just "make" and without any
additional configuration. It fails with the following error message:

/home/svanders/mirage/muen/tools/mupack/bin/mupack -i
/home/svanders/mirage/muen/policy/obj -o
/home/svanders/mirage/muen/pack/obj
/home/svanders/mirage/muen/pack/obj/policy_b.xml
Sep 12 2017 14:24:11 mupack: Looking for input files in
'/home/svanders/mirage/muen/policy/obj'
Sep 12 2017 14:24:11 mupack: Using output directory
'/home/svanders/mirage/muen/pack/obj'
Sep 12 2017 14:24:11 mupack: Processing policy
'/home/svanders/mirage/muen/pack/obj/policy_b.xml'
Sep 12 2017 14:24:11 mupack: Registered pre-check(s) 3
Sep 12 2017 14:24:11 mupack: Registered post-check(s) 1
Sep 12 2017 14:24:11 mupack: Registered content provider(s) 2
Sep 12 2017 14:24:11 mupack: Checking existence of 63 file(s)
Sep 12 2017 14:24:11 mupack: Processing failed, aborting
Sep 12 2017 14:24:11 mupack: File
'/home/svanders/mirage/muen/policy/obj/initramfs.cpio.xz' too large for
physical memory region 'initramfs': 16#0035_6ef0# > 16#0030_0000#
make[1]: *** [Makefile:19: /home/svanders/mirage/muen/pack/obj/muen.img]
Error 1
make[1]: Leaving directory '/home/svanders/mirage/muen/pack'
make: *** [Makefile:31: pack] Error 2

I saw the initramfs is downloaded from somewhere else, so maybe it has
been getting bigger and now doesn't fit into a static partition? What
would I have to adapt, to make it work?

The full build logs are attached.

Thanks in advance for any advice!

Best regards

Sven

[Adrian-Ken Rueegsegger]

Hello and welcome to the list,

On 09/12/2017 10:50 PM, Sven Anderson wrote:
> first of all, thanks for that great work and project!

Thanks, glad you like it!

> I'm trying to build the demo image with just "make" and without any
> additional configuration. It fails with the following error message:

[snip]

> Sep 12 2017 14:24:11 mupack: File
> '/home/svanders/mirage/muen/policy/obj/initramfs.cpio.xz' too large for
> physical memory region 'initramfs': 16#0035_6ef0# > 16#0030_0000#
> make[1]: *** [Makefile:19: /home/svanders/mirage/muen/pack/obj/muen.img]
> Error 1
> make[1]: Leaving directory '/home/svanders/mirage/muen/pack'
> make: *** [Makefile:31: pack] Error 2
>
> I saw the initramfs is downloaded from somewhere else, so maybe it has
> been getting bigger and now doesn't fit into a static partition? What
> would I have to adapt, to make it work?

That is indeed the case as the initramfs image has been updated to keep
up with the continued development of the devel branch.

If you are using the current master (commit 1924045...) then you can try
downloading this image [1] and setting the environment variable
INITRAMFS to the path of the downloaded file.

However I would suggest you checkout the devel branch instead, where
everything should work as expected.

Hope this helps.

Regards,
Adrian

[1] -
https://github.com/codelabs-ch/buildroot-muen/raw/aed6f028ea426716b1d5e517d79fc8a42729af96/initramfs.cpio.xz

[Sven Anderson]

Hi Adrian!

On 12.09.2017 16:24, Adrian-Ken Rueegsegger wrote:
> However I would suggest you checkout the devel branch instead, where
> everything should work as expected.

Thanks, that worked. Although, I had to run it with `make NUM_CPUS=1`,
because otherwise the gnatwhy3 or why3sever was hanging sometimes.
(Maybe related to the bug addressed here:
https://github.com/AdaCore/why3/commit/f2cbded5da7a3fcbebb61ee98b8e6c8d9c1d2227

Other than that: I have a muen image now, thanks! Let's see if i can
make use of it now. :-)

Cheers,

Sven

[Adrian-Ken Rueegsegger]

Hi,

On 09/14/2017 12:26 AM, Sven Anderson wrote:
> On 12.09.2017 16:24, Adrian-Ken Rueegsegger wrote:
>> However I would suggest you checkout the devel branch instead, where
>> everything should work as expected.
>
> Thanks, that worked. Although, I had to run it with `make NUM_CPUS=1`,
> because otherwise the gnatwhy3 or why3sever was hanging sometimes.
> (Maybe related to the bug addressed here:
> https://github.com/AdaCore/why3/commit/f2cbded5da7a3fcbebb61ee98b8e6c8d9c1d2227

Glad to hear that it works now. What version of the SPARK tools are you
using?

Note, that there is also the NO_PROOF environment variable. If you set
it, then the SPARK proofs will be skipped:

$ make NO_PROOF=true emulate

Regards,
Adrian

[Sven Anderson]

Hi Adrian

On 14.09.2017 01:38, Adrian-Ken Rueegsegger wrote:
> Glad to hear that it works now. What version of the SPARK tools are you
> using?
>
> Note, that there is also the NO_PROOF environment variable. If you set
> it, then the SPARK proofs will be skipped:
>
> $ make NO_PROOF=true emulate

Good to know. Thanks!

BTW: I started the image (created with plain "make") with this grub entry:

menuentry "Muen" {
multiboot /muen.img
}

but when I start it like that, the keyboard (Lenovo T450s) doesn't
really work. If I enter "ps" after a while I get a long list of "pppppp"
and "ssssssss". Can I fix that with an additional grub config?

And in general: I want to use muen as a hypervisor for a mirageOS
unikernel, thanks to your solo5 integration. What is the best
development environment for this situation. Can I also run the unikernel
in the emulator? Is there a way to run the whole thing in a vm itself,
like kvm or virtualbox, with nested VMs? (Or is that what bochs is
actually doing?)

Thanks for your support,

Sven

[Adrian-Ken Rueegsegger]

Hello,

On 09/14/2017 07:59 PM, Sven Anderson wrote:
>
> BTW: I started the image (created with plain "make") with this grub entry:
>
> menuentry "Muen" {
> multiboot /muen.img
> }
>
> but when I start it like that, the keyboard (Lenovo T450s) doesn't
> really work. If I enter "ps" after a while I get a long list of "pppppp"
> and "ssssssss". Can I fix that with an additional grub config?

Muen system images are built for a specific hardware platform using XML
hardware descriptions. See also the toolchain document [1] which
explains the build process in detail. You can find the currently
included hardware specs in the policy/hardware/ directory.

The reason for the behavior you are seeing is that the default hardware
description used for building the image is for Bochs which specifies a
processor speed of 50 MHz. When running this image on hardware the
timing will be off so that is why you see key bounce when typing.

So in order to run a Muen system on the Lenovo T450s you will have to
create a hardware (and platform) description. We have a tool you can run
under Linux on the target hardware for the purpose of generating a
hardware description, see [2]. Once you have the XML file you could copy
it to policy/hardware/lenovo-t450s.xml.

As a next step you also need to provide a platform description. I would
guess that simply copying T440s one should be fine:

$ cp policy/platform/lenovo-t440s.xml policy/platform/lenovo-t450s.xml

Finally you can build an image for the T450s like so:

$ make HARDWARE=hardware/lenovo-t450s.xml SYSTEM=xml/demo_system.xml iso

> And in general: I want to use muen as a hypervisor for a mirageOS
> unikernel, thanks to your solo5 integration. What is the best
> development environment for this situation. Can I also run the unikernel
> in the emulator? Is there a way to run the whole thing in a vm itself,
> like kvm or virtualbox, with nested VMs? (Or is that what bochs is
> actually doing?)

Currently, nested virtualization is not a stable option because KVM
cannot run Muen reliably. Solo5/MirageOS unikernels that do not require
hardware access can be executed using Bochs. As Solo5 support has not
yet been merged into Muen devel you need to switch to the devel-mirage
branch.

Except for a few minor adjustments the description given in [3] should
still be valid. Since the solo5 and ocaml-freestanding patches have been
merged there is no need to pin these two MirageOS packages to the
codelabs-ch repositories. The third pin is still required though, see
also [4],[5].

Hope the hints and references are helpful and get you started.

Regards,
Adrian

[1] - https://muen.codelabs.ch/muen-toolchain.pdf
[2] - https://git.codelabs.ch/?p=muen/mugenhwcfg.git
[3] - https://github.com/Solo5/solo5/pull/190#issue-221060023
[4] - https://github.com/Solo5/solo5/issues/217
[5] - https://github.com/Solo5/solo5/issues/194