new_stack_size = new_tso_size - TSO_STRUCT_SIZEW;
IF_DEBUG(scheduler, fprintf(stderr,"increasing stack size from %d words to %d.\n", tso->stack_size, new_stack_size));
new_stack_size = new_tso_size - TSO_STRUCT_SIZEW;
IF_DEBUG(scheduler, fprintf(stderr,"increasing stack size from %d words to %d.\n", tso->stack_size, new_stack_size));