Our tool nbdfuse lets you mount an NBD block device as a file, using Linux FUSE. For example you could create a directory with a single file in it (called nbd) which contains the contents of the NBD export:
Frama-C is a giant modular system for writing formal proofs of C code. For months I’ve been on-and-off trying to see if we could use it to do useful proofs for any parts of the projects we write, like qemu, libvirt, libguestfs, nbdkit etc. I got side-tracked at first with this frama-c tutorial which is fine, but I got stuck trying to make the GUI work.
You have to give all the include directories and define out some qemu-isms.
The first time you run it, this won’t work for “reasons”. You have to initialize the why3 verifier using:
why3 config --full-config
Really frama-c should just do this for you, or at least tell you what you need to do in the obscure error message it prints.
This still won’t work because util/range.c includes glib headers which use GCC attributes and builtins and frama-c simply cannot parse any of that. So I ended up hacking on the source to replace the headers with standard C headers and remove the one glib-based function in the file.
At this point it does compile and the frama-C WP plugin runs. Of course without having added any annotations it simply produces a long list of problems. Also it takes a fair bit of time to run, which is interesting. I wonder if it will get faster with annotations?
That’s as far as I’ve got for the moment. I’ll come back later and try to add annotations.
I got Fedora 32 installed on an RPi 4 8GB, booting off USB, with UEFI and ACPI. I followed Robert Grimm’s instructions here, and had an additional set of complications summarised here. There’s not much to say except that it was fiendishly complicated. But it works beautifully now, and is reasonably quick too especially when you consider how little it cost.
So let’s talk about costs (all include tax and delivery):
Raspberry Pi 4 8GB
SanDisk 500GB SSD x 2
small SD card needed for booting
Only one of the SSDs is actually used, but if you follow Robert’s instructions you will need two. I didn’t have any external USB SSDs that were both USB 3 and not spinning hard disks, so I had to buy these, but I’ll be able to reuse one in a future project. The SD card is required to work around a bug in the UEFI firmware, but I happened to have one lying around.
We ported nbdkit to Windows. That port is now upstream and should appear in the next stable release (1.24). There is also a new native file plugin for Windows which supports Windows files and volumes, hole punching for sparse files, querying file sparseness, and efficient zeroing.
This week I ported nbdkit, our high performance plugin-based Network Block Device server, to Windows. Currently it’s not upstream but you can download the Windows branch from here.
There were several possible ways we could have done this including Cygwin which might have been easier, but in the end I did a port to the raw Win32/Winsock APIs. You can compile it on Fedora using the mingw-w64-based Fedora Windows Cross Compiler and run it using Wine. Familiar commands like this work:
I got many existing plugins and filters compiled. Not all of those listed will be working, but the main features are fine. You can also write your own plugins to the same API as Linux ones. I’m hoping that someone can write a Windows block device plugin (especially one which integrates with features like VSS).
AMD Zen 2 laptops are a thing, and they’re blazingly fast.
I just bought the HP Envy x360 which has a 6 core AMD Ryzen 5 4500U. Measuring some real world compiles it’s comfortably two and half times faster than my year old Intel-based Thinkpad T480s (which has 4 cores but 8 threads, and cost at least twice as much).
$ tar tf rhel.ova
Since tar files usually store their content unmangled, this opens an interesting possibility for reading (or even writing) the embedded disk image without needing to unpack the tar. You just have to work out the offset of the disk image within the tar file. virt-v2v has used this trick to save a copy when importing OVAs for years.
nbdkit has also included a tar plugin which can access a file inside a local tar file, but the problem is what if the tar file doesn’t happen to be a local file? (eg. It’s on a webserver). Or what if it’s compressed?
To fix this I’ve turned the plugin into a filter. Using nbdkit-tar-filter you can unpack even non-local compressed tar files:
nbdkit is our high performance Network Block Device server for serving disk images from unusual sources. One (usual) source for Linux installers is to download an ISO from a website like Get Fedora or debian.org. However that costs the host money and is also a central point of failure, so another way to download Linux installers is over BitTorrent. Many Linux distros offer torrents of their installers including Fedora and Debian. By using these you are helping to redistribute Linux and defraying the cost of hosting these ISOs.
So what’s the serious use for this? It has the interesting property that the more people who are installing your Linux distro, the less bandwidth it uses and the faster it runs! This could be interesting technology for any kind of distributed environment where you have lots of machines accessing the same fixed/read-only filesystem or disk image.
If you want to get started with nbdkit it’s already in all popular Linux distributions, and compiles from source on Linux, FreeBSD and OpenBSD.
This lead me to think about the RAM disk implementation in nbdkit. In nbdkit up to 1.20 it supports giant virtual disks up to 8 exabytes using a sparse array implemented with a 2-level page table. However it’s still a RAM disk and so you can’t actually store more real data in these disks than you have available RAM (plus swap).
But what if we compressed the data? There are some fine, very fast compression libraries around nowadays — I’m using Facebook’s Zstandard — so the overhead of compression can be quite small, and this lets you make limited RAM go further.
Compression ratios can be really good. I tested this by creating a RAM disk and filling it with a filesystem containing text and source files, and was getting 10:1 compression. (Note that filesystems start with very regular, easily compressible metadata, so you’d expect this ratio to quickly drop if you filled the filesystem up with a lot of files).
The compression overhead is small, although the current nbdkit-memory-plugin isn’t very smart about locking so it has rather poor performance under multi-threaded loads anyway. (A fun little project to fix that for someone who loves pthread and C.)
I also implemented allocator=malloc which is a non-sparse direct-mapped RAM disk. This is simpler and a bit faster, but has rather obvious limitations compared to using the sparse allocator.
I am Richard W.M. Jones, a computer programmer. I have strong opinions on how we write software, about Reason and the scientific method. Consequently I am an atheist [To nutcases: Please stop emailing me about this, I'm not interested in your views on it] By day I work for Red Hat on all things to do with virtualization. I am a "citizen of the world".
My motto is "often wrong". I don't mind being wrong (I'm often wrong), and I don't mind changing my mind.
This blog is not affiliated or endorsed by Red Hat and all views are entirely my own.