It's not only used when deleting a thread any more. Swapping fpuRelease and dissociateVCPUTCB makes no practical difference as they are independent, but it simplifies verification slightly. Signed-off-by: Indan Zupancic <indan@nul.nu>