For uniprocessor we have a complete ready JPF model for solving nested mutex problem. JPF-Code: https://github.com/saurabhgadia4/lock-model/tree/rtemsjpf-0.1
Avoid unwanted irrelevant commit messages!! The code is still in raw stage but solves all the potential cases of nested mutex problem. For SMP we already have locking for mutex related operations: _Thread_queue_Acquire_critical( &the_mutex->Wait_queue, lock_context ); This ticket lock is always acquired before performing any write operations in mutex_seize and mutex_surrender which are required for solving nested_mutex problem. So for SMP we just have to overcome the data race that might happen while modifying thread->real_priority. Thanks, Saurabh Gadia On Wed, Jul 15, 2015 at 4:49 PM, Saurabh Gadia <ga...@usc.edu> wrote: > Hi, > Is there any explicit locking to avoid data races condition on members of > Thread_Control_struct in rtems? As for mutex we have ticket_lock over its > wait_queue in SMP architecture which can serve as explicit locking in > mutex. For thread I feel data race condition may happen while setting > *thread->current_priority. > *As it is updated by thread while restoring its priority and while some > other thread trying to promote for nested_mutex behavior. > > Thanks, > > Saurabh Gadia >
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel