/* Note that CURRENT_TIME may perform an unsafe call */
TIME now = CURRENT_TIME;
TSO_EXECTIME(CurrentTSO) += now - TSO_BLOCKEDAT(CurrentTSO);
/* Note that CURRENT_TIME may perform an unsafe call */
TIME now = CURRENT_TIME;
TSO_EXECTIME(CurrentTSO) += now - TSO_BLOCKEDAT(CurrentTSO);