news
Kernel Space: Xen and Intel Defective Chips Getting Slower
-
Thomas Leondard ☛ Proving liveness with TLA
The vchan protocol is used for efficient communication between Xen virtual machines. In 2018, I made a TLA+ specification of vchan: I created a specification of the protocol from the C code, used the model checker (TLC) to test that the protocol worked on small models, and wrote a machine-verified proof of Integrity (that the data received always matched what was sent). I also outlined a proof of Availability (that data sent will eventually arrive, rather than the system deadlocking or going around in circles). But: [...]
-
FUDZilla ☛ Linux updates made “Meteor Lake” slower
Phoronix reran its launch tests on the same Acer Swift Go 14 it bought at release, checking what two years of kernel, compiler and driver churn did to performance ahead of Panther Lake laptop noise at CES 2026.
The December 2023 baseline used Ubuntu 23.10, Linux 6.7 and Mesa 24.0-devel graphics drivers via the Oibaf PPA. The end-of-2025 retest moved to an Ubuntu 26.04 daily build with Linux 6.18, GCC 15.2 and Mesa 25.2.
Phoronix kept the comparison honest by sticking to 215 benchmarks that still build and run cleanly on the newer stack. That should have been the easy part.