Hello Genodians,

I have spent the last few months familiarizing myself with the base API and 
creating some sample projects. While I am relatively new to Genode, I had a few 
ideas during my initial exploration for areas to which I might contribute.

[1] When I was just starting out, my biggest challenge was the build system. 
While going through some of the basic examples / demos, I developed a rather 
simplistic Nix wrapper around the Genode build system (see [a]). Despite its 
simplicity, it greatly sped up my development time. For those that aren't 
familiar, Nix is a language for creating reproducible builds (see [b]). I was 
able to get several of my co-workers spun up on my projects in a single 
command. Since Nix has a docker image, creating development container images 
for those that did not already have Nix was trivial. I think there is a lot of 
potential here for decreasing the barrier to entry for playing with Genode demo 
scenarios, and generally making Genode builds more reproducible.

In my cursory research, I came across at least one past attempt at porting the 
Genode build system to Nix and vice versa (see [c]), as well as a mailing list 
discussion from almost a decade ago (see [d]). Has anyone continued these 
efforts? If no one is currently working on this, would it be something that 
others would be interested in using? I have my own ideas for how I would 
implement this, but I would like to get input from more experienced members of 
the community.

[2] I also want to ask about system composition abstractions. XML ROMs make 
sense as a runtime representation since they are easy to parse, but they make 
it difficult to write complex system configurations by hand. Are there any 
current efforts to create build and/or runtime abstractions for system 
composition? From my naive perspective, this also seems like a wonderful place 
to introduce a high-level package manager to create and deploy modular 
subsystems (if one doesn't already exist). I also wonder if there are any 
opportunities here for formal modelling and analysis of a configuration.

[3] Finally, I want to ask about any previous or planned work to formally 
verify the correctness of important Genode components (e.g, core, init) and the 
Genode API. Are there any challenges that make this infeasible? There are 
several follow-up questions I would have before going in this direction, but I 
would once again like to get input before adding my thoughts.

To summarize:
1. Has anyone been working on porting Genode to Nix (or vice versa)?
2. Is anyone working on a build and/or runtime abstraction for system 
composition?
3. Is there any ongoing or planned work toward formal verification of Genode 
components (e.g., core, init, etc.)?

I look forward to hearing everyone's thoughts!

Best,
Zachary Zollers

[a] https://github.com/zgzollers/nixpkgs-genode
[b] https://nixos.org/
[c] 
https://discourse.nixos.org/t/genodepkgs-extending-nixpkgs-nixos-to-genode/8779
[d] 
https://lists.genode.org/mailman3/hyperkitty/list/users@lists.genode.org/message/QUNDVXAHGSSI5BA2PEB573DU67ZFKDOX/
_______________________________________________
users mailing list -- users@lists.genode.org
To unsubscribe send an email to users-le...@lists.genode.org
Archived at 
https://lists.genode.org/mailman3/hyperkitty/list/users@lists.genode.org/message/WBKYRPJNYEBOMQ4WRTSIZZ2HQREJZ6YU/

Reply via email to