Thanks for posting the updated version. This quote…

“At initialization time, DPDK may crash if the first 128 CPU cores are all disabled [7]. It looks for the first enabled core, but does not check for the case where it does not find any enabled core before giving up, with a default limit of 128. If no core is available, DPDK performs an out-of-bounds memory access, which is likely to cause a crash. “

…is a nice example of what model-checking or verification can show that might be ridiculously hard to find with review and/or testing. The bug seems like an unlikely situation that shows little value to strong verification for people considering learning such techinques. If you generalize the wording, some process activates with no access to each thing it tried to access and then does something that might crash. Now, that general pattern sounds like something that is likely to happen in someone’s app due to access control, network being down, a recovery procedure activating after stuff has failed, a firmware function activates before workhorse CPU’s are ready to execute. and so on. Maybe you won’t run into a situation where you check 128 cores but catch-all analyses can help in other situations you might run into.