Improve mutex usage verification framework for the 4.0 threading interface #206

New issue

Open

opened 2025-09-05 04:24:13 -05:00 by gilles-peskine-arm · 0 comments

gilles-peskine-arm commented

2025-09-05 04:24:13 -05:00

(Migrated from github.com)

We've made changes to the threading abstraction starting with TF-PSA-Crypto 1.0 (issue, 4.0.0.0 interface and associated framework changes).

The new threading abstraction doesn't mesh well with the mutex usage verification framework. In my prototype (which had broader changes to the threading abstraction), I tried to have threading_helpers.c cope with both the old and the new interface through a lot of ifdefs, but it became quite messy. In the updated version, it's less messy and passes the CI, but still has some hacks where the new code is trying to fit into the shape of the old code.

For this rework, I think the right way is to redesign how the usage verification code hooks into the library, not just in TF-PSA-Crypto but also in Mbed TLS 3.6. (This is guarded by MBEDTLS_TEST_HOOKS so we can change things in the LTS.)

The primary goal of this issue is to make the mutex usage verification framework easier to understand, in particular from the point of view of a library maintainer who sees a test failure and needs to figure out what's failing and why. A related goal is to have the verification framework work with MBEDTLS_THREADING_ALT, which has its own issue https://github.com/Mbed-TLS/mbedtls-framework/issues/207.

We've made changes to the threading abstraction starting with TF-PSA-Crypto 1.0 ([issue](https://github.com/Mbed-TLS/mbedtls/issues/8455), [4.0.0.0 interface](https://github.com/Mbed-TLS/TF-PSA-Crypto/pull/434) and [associated framework changes](https://github.com/Mbed-TLS/mbedtls-framework/pull/204)). The new threading abstraction doesn't mesh well with the mutex usage verification framework. In my [prototype](https://github.com/Mbed-TLS/TF-PSA-Crypto/pull/415) (which had broader changes to the threading abstraction), I tried to have `threading_helpers.c` cope with both the old and the new interface through a lot of ifdefs, but it became quite messy. In the updated version, it's less messy and passes the CI, but still has some hacks where the new code is trying to fit into the shape of the old code. For this rework, I think the right way is to redesign how the usage verification code hooks into the library, not just in TF-PSA-Crypto but also in Mbed TLS 3.6. (This is guarded by `MBEDTLS_TEST_HOOKS` so we can change things in the LTS.) The primary goal of this issue is to make the mutex usage verification framework easier to understand, in particular from the point of view of a library maintainer who sees a test failure and needs to figure out what's failing and why. A related goal is to have the verification framework work with `MBEDTLS_THREADING_ALT`, which has its own issue https://github.com/Mbed-TLS/mbedtls-framework/issues/207.

No milestone

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

gh-Mbed-TLS/mbedtls-framework#206

No description provided.

Rows
Columns