mutex requirements #35

nashif · 2024-03-25T16:55:22Z

high-level: refine mutex requirement
mutex: add requirements for a mutex

Mutex functional requirements. Signed-off-by: Anas Nashif <[email protected]>

gregshue · 2024-03-27T14:13:50Z

docs/zephyr_02_functional_requirements.sdoc

+STATEMENT: >>>
+While a thread needs exclusive access to a shared resource, the Zephyr RTOS
+shall provide a mechanism to lock a mutex.
+<<<


Remove the While clause. The mechanism needs to always be provided.

"The Zephyr RTOS shall provide a mechanism for a thread to lock a mutex."

gregshue · 2024-03-27T14:14:58Z

docs/zephyr_02_functional_requirements.sdoc

+When a mutex is successfully locked by a thread, the Zephyr RTOS shall ensure
+that the mutex becomes unavailable for locking by other threads until it is
+unlocked.
+<<<


How do you verify "ensure"? Can the verification be automated?

yeah, we already have tests verifying this.

I do you test that something is ensured rather than just that it happens?

Restate without superfluous infinitives per INCOSE GtWR R10.

Does this still cover the current implementation?
"When a mutex is locked by a thread,
that mutex is unavailable for locking by other threads
the mutex retains the thread is the owning thread"

I am not sure if this second RQT is needed and seperate from the first. Isn't this the very nature of a Mutex to be lockable by one and only one thread at the same time always?

That the same thread can lock the same Mutex multiple times is different though and probably covered elswhere, too.

gregshue · 2024-03-27T14:15:34Z

docs/zephyr_02_functional_requirements.sdoc

+STATEMENT: >>>
+While a thread no longer requires exclusive access to a shared resource, the
+Zephyr RTOS shall provide a mechanism to unlock a mutex.
+<<<


Remove the While clause. The mechanism needs to always be provided.

"The Zephyr RTOS shall provide a mechanism for the owning thread to unlock a mutex."

I second with Tims suggestion for the RQT.

gregshue · 2024-03-27T14:16:26Z

docs/zephyr_02_functional_requirements.sdoc

+STATEMENT: >>>
+When a mutex is successfully unlocked by a thread, the Zephyr RTOS shall ensure
+that the mutex becomes available for locking by other threads.
+<<<


How do you verify "ensure"? Can the verification be automated?

yes, we test for this already.

Restate without superfluous infinitives per INCOSE GtWR R10.

I think this requirement is intended to cover the atomic mutex operation of unlocking and then locking for the next waiting thread.

If so, I suggest:
"When a mutex is unlocked and another thread waiting to lock that mutex, the unlock and lock operations shall be atomic"

gregshue · 2024-03-27T14:20:02Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Timed locking of a Mutex
+STATEMENT: >>>
+Mutexes shall support timed locking, where threads can specify a timeout period for waiting on the mutex.
+<<<


You just changed abstraction levels. "the Zephyr RTOS shall" is a different level than "Mutexes shall".

Rephrase to remove "where". Reserve "where" for preconditions.

Seems like the Semaphore requirements covering timeouts should be duplicated for mutexes.

For consistency of language this RQT should also start with "The Zephyr RTOS shall support ..." the more consistent RQTs are written the easier they become to parse (by humans and non-humans alike)

gregshue · 2024-03-27T14:31:48Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Priority Inheritance
+STATEMENT: >>>
+When using mutexes for resource synchronization, the Zephyr RTOS shall implement priority inheritance protocols to prevent priority inversion scenarios.
+<<<


Remove the While clause. The mechanism needs to always be provided.

"shall implement" is not an observable behavior. Are you intentionally trying to constrain the implementation? If so, how do you verify this? Can verification be automated?

please provide a suggestion on the wording. I do not see any other way this can
be expressed. You keep asking about automation of verification, not sure what
you mean by now, this is something that can be tested, yes, why are we talking
about automation? why is this relevant?

Mutexes are only used for resource synchronization, so remove the conditional.

"to prevent priority inversion scenarios" is justification. Remove it (INCOSE GtWR R20).

Priority inheritance is implied by mutex in an RTOS. I think this is a better description for the highest abstraction layers: "The Zephyr shall expose mutex services."

{sigh}

Automated verification helps fulfill a critical User Need: to be able to verify the OSS software with the User-provided qualified toolchain in a timely manner. There are 4 identified methods for verification: Test, Demonstration, Inspection, Analysis. Doing full verification manually takes FAR too long, so product integrators need automated verification suites to come with the OSS. The most natural verification type to automate is Test.

AFAICT the biggest enabler to deploying and updating secure systems is the rapid integration, revalidation, and deployment of security fixes. Product manufacturers soon will need to publicly commit to a specific response time to security issues (e.g., 30d, 60d, 90d). Component providers (e.g., Nordic, Zephyr Project) that commit to rolling out security fixes faster than the product manufacturer commitment remain as viable suppliers. Those that do not lose out on the design win.

Requirements need to be testable, fully agree with that and there is no argument. Automation is key and we need to get to almost 100% automation, sure thing.
Asking if the some requirement can be tested or verified is fine, however asking if "verification can be automated" is off-topic and I did not know what you mean because of that.

AFAICT the biggest enabler to deploying and updating secure systems is the rapid integration, revalidation, and deployment of security fixes. Product manufacturers soon will need to publicly commit to a specific response time to security issues (e.g., 30d, 60d, 90d). Component providers (e.g., Nordic, Zephyr Project) that commit to rolling out security fixes faster than the product manufacturer commitment remain as viable suppliers. Those that do not lose out on the design win.

This is going off-topic.

"Mutexes shall implement priority inheritance protocols."

Implement does not tell me how priority inheritance behaves. But the next two requirements address priority inheritance specifically.

gregshue · 2024-03-27T14:36:33Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Priority Inheritance - priority elevation
+STATEMENT: >>>
+When a higher-priority thread begins waiting on the mutex, the Zephyr RTOS shall temporarily elevate the priority of the owning thread.
+<<<


How is this distinct from the "Priority Inheritance" requirement above? If these are at different levels of detail then they need to reference each other.

Use "While" instead of "When". This condition is a state not an event.

"While a higher-priority thread is waiting on a mutex, the Zephyr RTOS shall elevate the priority of the owning thread."

gregshue · 2024-03-27T14:37:40Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Mutex Ownership
+STATEMENT: >>>
+Mutexes shall track the owning thread when locked to ensure exclusive access to the associated resource.
+<<<


Remove "to ensure ...". It is justification not observable behavior or condition.

"Mutexes shall track the owning thread when locked"

I think I made this a second part to ZEP-MUTEX-4 Exclusive Locking of a Mutex

gregshue · 2024-03-27T14:44:19Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Mutex Ownership - Unlock
+STATEMENT: >>>
+The Zephyr RTOS shall allow only the owning thread to unlock the mutex.
+<<<


Avoid using the word "only" in requirements. It is usually(?) very hard or impossible to verify.

In many cI think this is better phrased as:

While the mutex is not in a recursive lock,
When the thread owning a mutex requests to unlock it,
the ... shall ...

I think this is covered by my suggested wording for ZEP-MUTEX-5 Unlocking of a Mutex:
"The Zephyr RTOS shall provide a mechanism for the owning thread to unlock a mutex."

gregshue · 2024-03-27T14:45:17Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Priority Ceiling
+STATEMENT: >>>
+The Zephyr RTOS shall implement priority ceiling protocols to limit the extent of priority elevation during priority inheritance.
+<<<


Remove the justification phrase "to limit ...".

"shall implement" is not an observable behavior. Are you intentionally trying to constrain the implementation? If so, how do you verify this? Can verification be automated?

tobiaskaestner · 2024-04-18T14:50:03Z

docs/zephyr_02_functional_requirements.sdoc

@@ -960,25 +960,184 @@ As a Zephyr OS user I want to be able to exchange 1 to N data objects between di
 [/SECTION]

 [SECTION]
-TITLE: Mutex
+TITLE: Thread Syncronization


nitpick: Thread Synchronization

tobiaskaestner · 2024-04-18T14:54:08Z

docs/zephyr_02_functional_requirements.sdoc

+COMPONENT: Mutex
+TITLE: Locking of a Mutex
+STATEMENT: >>>
+While a thread needs exclusive access to a shared resource, the Zephyr RTOS


Suggestion: While the above RQTs begin with "The Zephyr RTOS ..." this one doesn't. Also the refernce to shared resource is probably a rationale. Consider rephrasing this RQT to read "The Zephyr RTOS shall provide a mechanism to lock a mutex so that no other thread can obtain the same Mutex while the mutex is locked. Rationale: This way threads can protect critical regions of code and prevent concurrent access to shared resources.

tobiaskaestner · 2024-04-18T14:56:29Z

docs/zephyr_02_functional_requirements.sdoc

+When a mutex is successfully locked by a thread, the Zephyr RTOS shall ensure
+that the mutex becomes unavailable for locking by other threads until it is
+unlocked.
+<<<


I am not sure if this second RQT is needed and seperate from the first. Isn't this the very nature of a Mutex to be lockable by one and only one thread at the same time always?

That the same thread can lock the same Mutex multiple times is different though and probably covered elswhere, too.

tobiaskaestner · 2024-04-18T14:56:57Z

docs/zephyr_02_functional_requirements.sdoc

+STATEMENT: >>>
+While a thread no longer requires exclusive access to a shared resource, the
+Zephyr RTOS shall provide a mechanism to unlock a mutex.
+<<<


I second with Tims suggestion for the RQT.

tobiaskaestner · 2024-04-18T14:58:23Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Timed locking of a Mutex
+STATEMENT: >>>
+Mutexes shall support timed locking, where threads can specify a timeout period for waiting on the mutex.
+<<<


For consistency of language this RQT should also start with "The Zephyr RTOS shall support ..." the more consistent RQTs are written the easier they become to parse (by humans and non-humans alike)

tobiaskaestner · 2024-04-18T14:58:38Z

docs/zephyr_02_functional_requirements.sdoc

+STATUS: Draft
+TYPE: Functional
+COMPONENT: Mutex
+TITLE: Indifinite locking of a Mutex


nitpick: Indefinite

tobiaskaestner · 2024-04-18T15:01:24Z

docs/zephyr_02_functional_requirements.sdoc

+TITLE: Indifinite locking of a Mutex
+STATEMENT: >>>
+Mutexes shall support indefinite locking allowing threads to wait indefinitely until the mutex becomes available.
+<<<


Not sure if we are running into semantic non-sense land (pun intended) but indefinite and K_FOREVER are pretty much the same thing for me. Using words not stemming from the actual implementation has the added advantage that we do not bind the RQTs too strongly to the implementation.

Timotheous · 2024-05-14T21:51:08Z

I would hate to lose the work that has been done on this PR.
The nature of the "discussion" has made it hard for the owner to implement any changes.

Even without changes, it is better than the near empty file it will replace.

mutex: add requirements for a mutex

a5ed580

Mutex functional requirements. Signed-off-by: Anas Nashif <[email protected]>

nashif force-pushed the topic/req/mutex branch from f11e66d to a5ed580 Compare March 25, 2024 18:29

gregshue suggested changes Mar 27, 2024

View reviewed changes

tobiaskaestner reviewed Apr 18, 2024

View reviewed changes

simhein added the Requirements Requirements work label May 13, 2024

mutex requirements #35

Are you sure you want to change the base?

mutex requirements #35

Conversation

nashif commented Mar 25, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gregshue Mar 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Timotheous Apr 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Timotheous Apr 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Timotheous commented May 14, 2024

gregshue Mar 27, 2024 •

edited

Loading

Timotheous Apr 2, 2024 •

edited

Loading

Timotheous Apr 2, 2024 •

edited

Loading