what should I read if I want to understand the verification of concurrent programs related to the sel4 project?