seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
25 stars 63 forks source link

Test SCHED0021 has a race condition #42

Closed axel-h closed 1 year ago

axel-h commented 3 years ago
    /* Configure all of the threads */
    for (size_t thread = 0; thread < PREEMPTION_THREADS; thread += 1) {
[...]
        /* Thread must run at same prio as monitor */
        set_helper_priority(env, &threads[thread], OUR_PRIO);
[...]
    }
[...]
    /* Start executing other threads */
    ZF_LOGD("Releasing Threads");
    test_simple_preempt_start = 1;
    /* Yield should cause all other threads to execute before returning
     * to the current thread. */
    seL4_Yield();

Isn't there a tiny chance that the preemptive scheduler will kick in after test_simple_preempt_start = 1? So all threads get their time slice to run. Then seL4_Yield() is executed and each thread again gets a time slice to run? Wouldn't is be better to do this:

    /* Start executing other threads */
    ZF_LOGD("Releasing Threads");
    /* Release our time slice now to get a new one. That should ensure we are
     * not interrupted due to bad luck by the preemptive scheduler right after 
     * setting test_simple_preempt_start to 1 and then voluntarily yielding. For
     * the same reason we are also printing the doing the ZF_LOGD() above 
     * already.
     */
    seL4_Yield();
    /* Set a timeout for the test. Each thread should run for one tick. */
    uint64_t start = time_now(env);
    test_simple_preempt_start = 1;
    /* Yield should cause all other threads to execute before returning
     * to the current thread. 
     */
    seL4_Yield();
    test_simple_preempt_start = 0;

There is still a risk because we can't be really sure what time_now(env) does and how long this may take.

Aside from this, the line

    uint64_t now = start;

is the original code seems quite useless to me, as nobody is using the value assigned to now, it is overwritten a few lines later. This might be a left over from a time where another debug message was printed with it?