seL4 / sel4test

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

SCHED0021 fails on star64 platform when config `LibUtilsDefaultZfLogLevel` is `0` #109

Closed canarysnort01 closed 1 year ago

canarysnort01 commented 1 year ago

I suspect the extra debug prints might be causing the timing measurements to be off.

I'm testing this on the pinetab-v hardware as described in https://github.com/seL4/seL4/pull/1019#issuecomment-1686518507.

When building sel4test like this, all is well in the universe:

../init-build.sh -DPLATFORM=star64 -DKernelRiscvExtD=true -DUseRiscVOpenSBI=false -DSIMULATION=false -DMCS=true -DSMP=false

Output: sel4test-star64-mcs.txt

However, when built with verbose logging, SCHED0021 fails:

../init-build.sh -DPLATFORM=star64 -DKernelRiscvExtD=true -DUseRiscVOpenSBI=false -DSIMULATION=false -DMCS=true -DSMP=false -DLibUtilsDefaultZfLogLevel=0

Output: sel4test-star64-mcs-verbose.txt

Indanz commented 1 year ago

I bet it works with the following fixes:

(Edit: I thought ZF_LOGD in the helper thread wasn't shown, but it's just swamped by the other output. It's the most likely cause.)

canarysnort01 commented 1 year ago

Oh, some of these changes have already been made recently, sorry for the confusion. My sel4test wasn't current. I will make the remaining changes.

canarysnort01 commented 1 year ago
  • The ZF_LOGD("Releasing Threads"); should be before the uint64_t start = time_now(env);.

  • There should be another yield call before test_simple_preempt_start = 1; and the start timestamp.

These have already been done recently and with these changes the tests pass on my hardware.

  • Remove all the ZF_LOGD calls from test_simple_preempt_runner() .

Do you want me to go ahead and make this change?

Indanz commented 1 year ago

Do you want me to go ahead and make this change?

If it passes with the other changes, just leave it for now.