Date: Mon, 12 Feb 2024 01:59:15 +0100 From: "lars.sonchocky-helldorf@hamburg.de" <lars.sonchocky-helldorf@hamburg.de> To: Mario Marietto <marietto2008@gmail.com> Cc: Mark Millard <marklmi@yahoo.com>, freebsd-arm <freebsd-arm@freebsd.org>, freebsd-hackers <freebsd-hackers@freebsd.org>, FreeBSD Current <freebsd-current@freebsd.org> Subject: Re: How to use the L4 Microkernel with a FreeBSD userland. Message-ID: <011B3051-E189-41AF-AAE7-9867010017C1@hamburg.de> In-Reply-To: <CA%2B1FSiiy7TD%2Bo=OxZESJr4ExDFajy1ZdkusJ%2BA50qb4WYqS0nQ@mail.gmail.com> References: <CA%2B1FSijq0ez9%2BJXCSJP2rfWUXLjcTaEPJo-3NcO5Vu3H26L=hg@mail.gmail.com> <071E080E-C0E6-40F0-A0DF-4FCC22FC004D@yahoo.com> <CA%2B1FSign02NftThWsgVVRV6Ec83-T1sATiUKh7dHmmoXzW-_mg@mail.gmail.com> <ACAAF976-6868-4A88-99CB-5254CDE6C81C@yahoo.com> <CA%2B1FSiiy7TD%2Bo=OxZESJr4ExDFajy1ZdkusJ%2BA50qb4WYqS0nQ@mail.gmail.com>
next in thread | previous in thread | raw e-mail | index | archive | help
--Apple-Mail=_AD026309-0ADD-46C2-B490-8CF26003A37D Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 hi Mario, I think the closest thing to what you=E2=80=99re aspiring to is the = =E2=80=9EDarbat=E2=80=9C-Kernel: a Darwin Kernel ported to L4: https://trustworthy.systems/publications/papers/Lee_Gray_06.abstract But then again the project is no longer active, Googling it brings a lot = of archived stuff. But still, it might work as an Inspiration (if you=E2=80=99re able to = dig up the sources, I didn=E2=80=99t look. Kind regards, Lars > Am 11.02.2024 um 22:20 schrieb Mario Marietto = <marietto2008@gmail.com>: >=20 > I will do it as soon as I get all the necessary tools to turn on the = Raspberry Pi 4b. I was thinking that L4 worked like the old project = coLinux,where Linux ran as a list of processes under WIndows. In my sick = mind I'd thought that L4 allows FreeBSD to run as a list of processes = with the L4 microkernel itself on "top" of it. Do you know if something = like this exists ?=20 >=20 >=20 >=20 > On Sun, Feb 11, 2024 at 9:01=E2=80=AFPM Mark Millard = <marklmi@yahoo.com <mailto:marklmi@yahoo.com>> wrote: >> [Only replying to what I've subscribed to --and I dropped >> Warner as well.] >>=20 >> On Feb 11, 2024, at 11:43, Mario Marietto <marietto2008@gmail.com = <mailto:marietto2008@gmail.com>> wrote: >>=20 >> > ok. But what does this mean ? That I can use whatever Linux distro = I want ? Or even the FreeBSD world ? >>=20 >> Only to build L4Re. >>=20 >> The LR4e built will not contain any Linux userland materials, >> nor any FreeBSD userland materials. LR4e has its own userland >> materials that will be present instead. >>=20 >> = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/ >>=20 >> already contains pre-built .elf and .uimage files Why not use one >> of those on the RPi4B? >>=20 >> By size (larger), the most complete ones for the RPi4B seem to be >> (both formats): >>=20 >> = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/boot= strap_vm-multi_rpi4.elf >> = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/boot= strap_vm-multi_rpi4.uimage >>=20 >> = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/boot= strap_vm-basic_rpi4.elf >> = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/boot= strap_vm-basic_rpi4.uimage >>=20 >>=20 >> > On Sun, Feb 11, 2024 at 7:59=E2=80=AFPM Mark Millard = <marklmi@yahoo.com <mailto:marklmi@yahoo.com>> wrote: >> >=20 >> >=20 >> > On Feb 11, 2024, at 05:44, Mario Marietto <marietto2008@gmail.com = <mailto:marietto2008@gmail.com>> wrote: >> >=20 >> > > I'm trying to understand how to use the L4 Microkernel with a = FreeBSD userland. I've asked the same to a L4 developer,but he told me = that he does not know FreeBSD,so I'm here to ask the same question. = First of all I'm sure that it can be done,because it is written clearly = on their website : >> > >=20 >> > >=20 >> > > http://os.inf.tu-dresden.de/L4Re/download/snapshots/ >> > >=20 >> > >=20 >> > > on the section : >> > > Host system requirements >> > > The host system shall be a 64bit-based system with a recent Linux = distribution installed and at least 2GB of free disk space. >> > > All necessary tools required by the build are available from the = provided packages of the Linux distributions, including cross compilers. = But there are also other cross compiler packages available (see below). = You might want to run make check_build_tools in the src/l4 directory to = verify the common tools are installed. >> > > You are free to use any Linux distribution you like, or even BSDs = or any of its derivatives. But then you should know the game. Especially = tool versions should be recent, as installed on the listed distributions = below. >> > > We are confident that the snapshot works on the following = distributions: >> > > =E2=80=A2 Debian 11 or later >> > > =E2=80=A2 Ubuntu 22.04 or later >> > >=20 >> > > Let's say I want to use the L4 microkernel + FreeBSD 14 on my = Raspberry Pi 4,the first step I did was to build L4Re for the = Rpi,according with this instructions : >> > >=20 >> > >=20 >> > > http://os.inf.tu-dresden.de/L4Re/rpi.html=20 >> > >=20 >> > > This is the log file of the compilation,that hasn't given any = error : >> > >=20 >> > >=20 >> > > https://pastebin.ubuntu.com/p/6SwN2mpJBM/ >> > >=20 >> > >=20 >> > > Or I could have taken a pre built image of the L4 microkernel = here :=20 >> > >=20 >> > >=20 >> > > = http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/arm64/ >> > >=20 >> > >=20 >> > >=20 >> > > At this point the tutorial says that I should use a Linux distro. = They suggest the official distro for the Raspberry Pi 4,that's RaspBian. = But I don't want to use Linux as a userland,I want to use FreeBSD. The = question now is : what should I do to achieve that goal ? How can I link = the L4 microkernel with the ubldr bootloader of FreeBSD ? Or should I = link it to the kernel of FreeBSD ? Can someone explain to me the missing = step ? thanks. >> >=20 >> > QUOTING the "Configuring yourself" section: >> > The make setup step configures predefined setups for both the L4Re = microkernel (Fiasco) and the L4Re user-level software, and connects both = together so the images for the target system can be built. >> > END QUOTE >> >=20 >> > So L4Re has its own user-level software, not just a kernel. There = is no use of a Linux or FreeBSD user-level software >> > when L4Re is booted. (They are just used for building.) >> >=20 >> > "The host system" is just a host for building the L4Re parts and = assembling the image from the parts. The "Pulling it together" section = is about combining the parts (including the microkernel and the = user-level software) to make the overall image that does not include = Linux or FreeBSD code. >>=20 >>=20 >> =3D=3D=3D >> Mark Millard >> marklmi at yahoo.com <http://yahoo.com/>; >>=20 >=20 >=20 > -- > Mario. --Apple-Mail=_AD026309-0ADD-46C2-B490-8CF26003A37D Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 <html><head><meta http-equiv=3D"content-type" content=3D"text/html; = charset=3Dutf-8"></head><body style=3D"overflow-wrap: break-word; = -webkit-nbsp-mode: space; line-break: after-white-space;"><div>hi = Mario,</div><div><br></div>I think the closest thing to what you=E2=80=99r= e aspiring to is the =E2=80=9EDarbat=E2=80=9C-Kernel: a Darwin Kernel = ported to L4:<div><br></div><div><a = href=3D"https://trustworthy.systems/publications/papers/Lee_Gray_06.abstra= ct">https://trustworthy.systems/publications/papers/Lee_Gray_06.abstract</= a></div><div><br></div><div>But then again the project is no longer = active, Googling it brings a lot of archived = stuff.</div><div><br></div><div>But still, it might work as an = Inspiration (if you=E2=80=99re able to dig up the sources, I didn=E2=80=99= t look.</div><div><br></div><div><br></div><div>Kind = regards,</div><div><br></div><div><span class=3D"Apple-tab-span" = style=3D"white-space:pre"> </span>Lars<br = id=3D"lineBreakAtBeginningOfMessage"><div><br><blockquote = type=3D"cite"><div>Am 11.02.2024 um 22:20 schrieb Mario Marietto = <marietto2008@gmail.com>:</div><br = class=3D"Apple-interchange-newline"><div><div dir=3D"ltr"><div>I will do = it as soon as I get all the necessary tools to turn on the Raspberry Pi = 4b. I was thinking that L4 worked like the old project coLinux,where = Linux ran as a list of processes under WIndows. In my sick mind I'd = thought that L4 allows FreeBSD to run as a list of processes with the L4 = microkernel itself on "top" of it. Do you know if something like this = exists ? </div><div><br></div><div><br> </div></div><br><div = class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Sun, Feb = 11, 2024 at 9:01=E2=80=AFPM Mark Millard <<a = href=3D"mailto:marklmi@yahoo.com">marklmi@yahoo.com</a>> = wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px = 0px 0px 0.8ex;border-left:1px solid = rgb(204,204,204);padding-left:1ex">[Only replying to what I've = subscribed to --and I dropped<br> Warner as well.]<br> <br> On Feb 11, 2024, at 11:43, Mario Marietto <<a = href=3D"mailto:marietto2008@gmail.com" = target=3D"_blank">marietto2008@gmail.com</a>> wrote:<br> <br> > ok. But what does this mean ? That I can use whatever Linux distro = I want ? Or even the FreeBSD world ?<br> <br> Only to build L4Re.<br> <br> The LR4e built will not contain any Linux userland materials,<br> nor any FreeBSD userland materials. LR4e has its own userland<br> materials that will be present instead.<br> <br> <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/</a><br> <br> already contains pre-built .elf and .uimage files Why not use one<br> of those on the RPi4B?<br> <br> By size (larger), the most complete ones for the RPi4B seem to be<br> (both formats):<br> <br> <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/bootstrap_vm-multi_rpi4.elf" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/bootstrap_vm-multi_rpi4.elf</a><br> <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/bootstrap_vm-multi_rpi4.uimage" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/bootstrap_vm-multi_rpi4.uimage</a><br> <br> <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/bootstrap_vm-basic_rpi4.elf" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/bootstrap_vm-basic_rpi4.elf</a><br> <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/bootstrap_vm-basic_rpi4.uimage" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/bootstrap_vm-basic_rpi4.uimage</a><br> <br> <br> > On Sun, Feb 11, 2024 at 7:59=E2=80=AFPM Mark Millard <<a = href=3D"mailto:marklmi@yahoo.com" = target=3D"_blank">marklmi@yahoo.com</a>> wrote:<br> > <br> > <br> > On Feb 11, 2024, at 05:44, Mario Marietto <<a = href=3D"mailto:marietto2008@gmail.com" = target=3D"_blank">marietto2008@gmail.com</a>> wrote:<br> > <br> > > I'm trying to understand how to use the L4 Microkernel with a = FreeBSD userland. I've asked the same to a L4 developer,but he told me = that he does not know FreeBSD,so I'm here to ask the same question. = First of all I'm sure that it can be done,because it is written clearly = on their website :<br> > > <br> > > <br> > > <a href=3D"http://os.inf.tu-dresden.de/L4Re/download/snapshots/"= rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/L4Re/download/snapshots/</a>= <br> > > <br> > > <br> > > on the section :<br> > > Host system requirements<br> > > The host system shall be a 64bit-based system with a recent = Linux distribution installed and at least 2GB of free disk space.<br> > > All necessary tools required by the build are available from = the provided packages of the Linux distributions, including cross = compilers. But there are also other cross compiler packages available = (see below). You might want to run make check_build_tools in the src/l4 = directory to verify the common tools are installed.<br> > > You are free to use any Linux distribution you like, or even = BSDs or any of its derivatives. But then you should know the game. = Especially tool versions should be recent, as installed on the listed = distributions below.<br> > > We are confident that the snapshot works on the following = distributions:<br> > > =E2=80=A2 Debian 11 or later<br> > > =E2=80=A2 Ubuntu 22.04 or later<br> > > <br> > > Let's say I want to use the L4 microkernel + FreeBSD 14 on my = Raspberry Pi 4,the first step I did was to build L4Re for the = Rpi,according with this instructions :<br> > > <br> > > <br> > > <a href=3D"http://os.inf.tu-dresden.de/L4Re/rpi.html" = rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/L4Re/rpi.html</a>; <br> > > <br> > > This is the log file of the compilation,that hasn't given = any error :<br> > > <br> > > <br> > > <a href=3D"https://pastebin.ubuntu.com/p/6SwN2mpJBM/" = rel=3D"noreferrer" = target=3D"_blank">https://pastebin.ubuntu.com/p/6SwN2mpJBM/</a><br>; > > <br> > > <br> > > Or I could have taken a pre built image of the L4 microkernel = here : <br> > > <br> > > <br> > > <a = href=3D"http://os.inf.tu-dresden.de/download/snapshots/pre-built-images/ar= m64/" rel=3D"noreferrer" = target=3D"_blank">http://os.inf.tu-dresden.de/download/snapshots/pre-built= -images/arm64/</a><br> > > <br> > > <br> > > <br> > > At this point the tutorial says that I should use a Linux = distro. They suggest the official distro for the Raspberry Pi 4,that's = RaspBian. But I don't want to use Linux as a userland,I want to use = FreeBSD. The question now is : what should I do to achieve that goal ? = How can I link the L4 microkernel with the ubldr bootloader of FreeBSD ? = Or should I link it to the kernel of FreeBSD ? Can someone explain to me = the missing step ? thanks.<br> > <br> > QUOTING the "Configuring yourself" section:<br> > The make setup step configures predefined setups for both the L4Re = microkernel (Fiasco) and the L4Re user-level software, and connects both = together so the images for the target system can be built.<br> > END QUOTE<br> > <br> > So L4Re has its own user-level software, not just a kernel. There = is no use of a Linux or FreeBSD user-level software<br> > when L4Re is booted. (They are just used for building.)<br> > <br> > "The host system" is just a host for building the L4Re parts and = assembling the image from the parts. The "Pulling it together" section = is about combining the parts (including the microkernel and the = user-level software) to make the overall image that does not include = Linux or FreeBSD code.<br> <br> <br> =3D=3D=3D<br> Mark Millard<br> marklmi at <a href=3D"http://yahoo.com/" rel=3D"noreferrer" = target=3D"_blank">yahoo.com</a><br> <br> </blockquote></div><br clear=3D"all"><br><span = class=3D"gmail_signature_prefix">-- </span><br><div dir=3D"ltr" = class=3D"gmail_signature">Mario.<br></div> </div></blockquote></div><br></div></body></html>= --Apple-Mail=_AD026309-0ADD-46C2-B490-8CF26003A37D--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?011B3051-E189-41AF-AAE7-9867010017C1>