Tag Archives: verification challenge

Verification Challenge 7: Heavy Modifications to Linux-Kernel Tree RCU

There was a time when I felt that Linux-kernel RCU was too low-level to possibly be the subject of a security exploit, but Rowhammer put paid to that naive notion. And it finally happened earlier this year. Now, I could … Continue reading

Posted in Uncategorized | Tagged , , , , , , , | Comments Off on Verification Challenge 7: Heavy Modifications to Linux-Kernel Tree RCU

Verification Challenge 7: Heavy Modifications to Linux-Kernel Tree RCU

There was a time when I felt that Linux-kernel RCU was too low-level to possibly be the subject of a security exploit, but Rowhammer put paid to that naive notion. And it finally happened earlier this year. Now, I could … Continue reading

Posted in Uncategorized | Tagged , , , , , , , | Comments Off on Verification Challenge 7: Heavy Modifications to Linux-Kernel Tree RCU

Verification Challenge 6: Linux-Kernel Tree RCU

It has been more than two years since I posted my last verification challenge, so it is only natural to ask what, if anything, has happened in the meantime. The answer is “Quite a bit!” I had the privilege of … Continue reading

Posted in Uncategorized | Tagged , , , , | Comments Off on Verification Challenge 6: Linux-Kernel Tree RCU

Verification Challenge 5: Uses of RCU

This is another self-directed verification challenge, this time to validate uses of RCU instead of validating the RCU implementations as in earlier posts. As you can see from Verification Challenge 4, the logic expression corresponding even to the simplest Linux-kernel … Continue reading

Posted in Uncategorized | Tagged , , , , | Comments Off on Verification Challenge 5: Uses of RCU

Verification Challenge 4: Tiny RCU

The first and second verification challenges were directed to people working on verification tools, and the third challenge was directed at developers. Perhaps you are thinking that it is high time that I stop picking on others and instead direct … Continue reading

Posted in Uncategorized | Tagged , , , , | Comments Off on Verification Challenge 4: Tiny RCU

Verification Challenge 3: cbmc

The first and second verification challenges were directed to people working on verification tools, but this one is instead directed at developers. It turns out that there are a number of verification tools that have seen heavy use. For example, … Continue reading

Posted in Uncategorized | Tagged , , , , | Comments Off on Verification Challenge 3: cbmc

Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

I suppose that I might as well get the “But what about Verification Challenge 1?” question out of the way to start with. You will find Verification Challenge 1 here. Now, Verification Challenge 1 was about locating a known bug. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

I suppose that I might as well get the “But what about Verification Challenge 1?” question out of the way to start with. You will find Verification Challenge 1 here. Now, Verification Challenge 1 was about locating a known bug. … Continue reading

Posted in Uncategorized | Tagged , , , , , | Comments Off on Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE

Stupid RCU Tricks: rcutorture Catches an RCU Bug

My previous posting described an RCU bug that I might plausibly blame on falsehoods from firmware. The RCU bug in this post, alas, I can blame only on myself. In retrospect, things were going altogether too smoothly while I was … Continue reading

Posted in Uncategorized | Tagged , , , | Comments Off on Stupid RCU Tricks: rcutorture Catches an RCU Bug