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]>

docs/zephyr_02_functional_requirements.sdoc

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?

docs/zephyr_02_functional_requirements.sdoc

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)

docs/zephyr_02_functional_requirements.sdoc

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

Uh oh!

Conversation

nashif commented Mar 25, 2024

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Timotheous Apr 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Timotheous Apr 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Timotheous commented May 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Timotheous Apr 2, 2024 •

edited

Loading

Timotheous Apr 2, 2024 •

edited

Loading