feat(threads): dynamic thread priorities

[elenaf9]

Description

Allow users to dynamically change thread priorities at runtime.

Issues/PRs references

Fixes #320
Depends on #437

Open Questions

Change checklist

• I have cleaned up my commit history and squashed fixup commits.
• I have followed the Coding Conventions.
• I have performed a self-review of my own code.
• I have made corresponding changes to the documentation.

[ROMemories]

Seems like the hax issue in CI (lack of support for let ... else statements) is now fixed upstream.
This is not picked up because we are currently pinning hax to an earlier version:

RIOT-rs/.github/workflows/hax.yml

Lines 14 to 18 in 2e84cce

	- name: ⤵ Install and configure hax
	uses: hacspec/hax-actions@main
	with:
	# pin hax to known-working
	hax_reference: d10f891a19f96bcafa9e31b1d78763e4f3cf30b4

[elenaf9]

Seems like the hax issue in CI (lack of support for let ... else statements) is now fixed upstream. This is not picked up because we are currently pinning hax to an earlier version:

RIOT-rs/.github/workflows/hax.yml

Lines 14 to 18 in 2e84cce

	- name: ⤵ Install and configure hax
	uses: hacspec/hax-actions@main
	with:
	# pin hax to known-working
	hax_reference: d10f891a19f96bcafa9e31b1d78763e4f3cf30b4

Thank you for pointing this out! I opened #378 to update our hax version.

[ROMemories]

I see that you've already reported a few months the hax issue the CI is currently failing with.

[elenaf9]

Still blocked by hacspec/hax#603.

[ROMemories]

Still blocked by hacspec/hax#603.

I suppose you could add a small position function helper in this module, implementing it by calling Iterator::next() manually, with a comment explaining why we don't use Iterator::position().

[elenaf9]

Rebased & addressed reviews. I also refactored the threads-dynamic-prios example into a test instead, because I think it's a simple API that doesn't require a separate example, but it's useful to have a test for the logic.

[elenaf9]

Still blocked by hacspec/hax#603.

I suppose you could add a small position function helper in this module, implementing it by calling Iterator::next() manually, with a comment explaining why we don't use Iterator::position().

I tried doing that with c969899, but unfortunately that then fails because early returns from loops aren't supported: hacspec/hax#196.
a117fc2 now implements it with a simple for-loop instead.

Edit: hmm, still doesn't work, no it fails because it doesn't know FnMut... next attempt: 33f723e.
Edit2: now fails because - Identifier not found: [v_ThreadId] even though I don't use it in any new places. Any idea why this error suddenly appear here? @ROMemories maybe?

[elenaf9]

Rebased & addressed the reviews. Hax check now also passes, thanks to @ROMemories!
Per #370 (comment), get_priority and set_priority now use RunqueueIds instead of u8.
The thread_create* functions should probably also use the RunqueueId, but that's out of scope for this PR, especially because it also involves changes in our macros.

[ROMemories]

Could you rebase on main? I'd like to test #437 on this PR 🙂

[ROMemories]

Could you rebase on main? I'd like to test #437 on this PR 🙂

Thanks! I checked the Actions logs and the lint job did error out as expected, as the previously present clippy warning is now considered an error, as expected since #437.

[kaspar030]

LGTM!