The synchronization in init and when passing contexts cross-task is sufficient to guarantee enough of an ordering that the values of VERIFY_IDX and MUTEXES will be visible when they should be.