Skip to content

mutex requirements #35

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

mutex requirements #35

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
181 changes: 170 additions & 11 deletions docs/zephyr_02_functional_requirements.sdoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

[REQUIREMENT]
UID: ZEP-91
UID: ZEP-MUTEX-1
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Mutex Kernel Object
TITLE: Initialization of Mutex at Compile time
STATEMENT: >>>
Zephyr shall support resource synchronization. (Note synchronization can be for memory access, and mutex may be one implementation, but not the only one).
The Zephyr RTOS shall provide a mechanism for defining and initializing mutexes
at compile time.
<<<
USER_STORY: >>>
As a Zephyr OS user I want to be able to sychonize threads when accessing common resources, where the thread shall have the option to:
- wait eternally until the resources becomes available.
- immediately return with a negative message if the resource is not available and allow the thread to continue.
- wait for a given time for the resource to become available or return with a negative message.

[REQUIREMENT]
UID: ZEP-MUTEX-2
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Initialization of Mutex at Runtime
STATEMENT: >>>
The Zephyr RTOS shall provide a mechanism for defining and initializing mutexes
at runtime time.
<<<
REVIEW_COMMENT: >>>
Concern over phrase recursive. What is it MUTEXing? Memory Management?

[REQUIREMENT]
UID: ZEP-MUTEX-3
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Locking of a Mutex
STATEMENT: >>>
While a thread needs exclusive access to a shared resource, the Zephyr RTOS
shall provide a mechanism to lock a mutex.
<<<

[REQUIREMENT]
UID: ZEP-MUTEX-4
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Exclusive Locking of a Mutex
STATEMENT: >>>
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.
<<<

[REQUIREMENT]
UID: ZEP-MUTEX-5
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Unlocking of a Mutex
STATEMENT: >>>
While a thread no longer requires exclusive access to a shared resource, the
Zephyr RTOS shall provide a mechanism to unlock a mutex.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I second with Tims suggestion for the RQT.


[REQUIREMENT]
UID: ZEP-MUTEX-6
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Availability of a Mutex after Unlocking
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.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes, we test for this already.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Restate without superfluous infinitives per INCOSE GtWR R10.

Copy link

@Timotheous Timotheous Apr 2, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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"


[REQUIREMENT]
UID: ZEP-MUTEX-7
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Timed locking of a Mutex
STATEMENT: >>>
Mutexes shall support timed locking, where threads can specify a timeout period for waiting on the mutex.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)


[REQUIREMENT]
UID: ZEP-MUTEX-8
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Indifinite locking of a Mutex
STATEMENT: >>>
Mutexes shall support indefinite locking allowing threads to wait indefinitely until the mutex becomes available.
<<<

[REQUIREMENT]
UID: ZEP-MUTEX-9
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Reentrant locking
STATEMENT: >>>
The Zephyr RTOS shall support reentrant locking, allowing a thread to lock a mutex it has already locked without causing a deadlock.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

", allowing ..." is descriptive text. Please remove it from the requirement statement.

Copy link

@Timotheous Timotheous Apr 2, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"The Zephyr RTOS shall support reentrant mutex locking."

Do we depend on common software engineering knowledge (and Google) or do we need more requirements describing the behavior of a entrant mutex.


[REQUIREMENT]
UID: ZEP-MUTEX-10
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Lock count
STATEMENT: >>>
Mutexes shall maintain a lock count to track the number of times a thread has locked the mutex.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems like an implementation detail. Is the current lock count exposed in an API?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is part of the mutex design in Zephyr and how it works, it is not an
implementation detail

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the key behavior of a reentrant mutex. So it is good.


[REQUIREMENT]
UID: ZEP-MUTEX-11
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Priority Inheritance
STATEMENT: >>>
When using mutexes for resource synchronization, the Zephyr RTOS shall implement priority inheritance protocols to prevent priority inversion scenarios.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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."

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

{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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

@Timotheous Timotheous Apr 2, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Mutexes shall implement priority inheritance protocols."

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


[REQUIREMENT]
UID: ZEP-MUTEX-12
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
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.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


[REQUIREMENT]
UID: ZEP-MUTEX-13
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Mutex Ownership
STATEMENT: >>>
Mutexes shall track the owning thread when locked to ensure exclusive access to the associated resource.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"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


[REQUIREMENT]
UID: ZEP-MUTEX-14
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Mutex Ownership - Unlock
STATEMENT: >>>
The Zephyr RTOS shall allow only the owning thread to unlock the mutex.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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."


[REQUIREMENT]
UID: ZEP-MUTEX-15
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Priority Ceiling
STATEMENT: >>>
The Zephyr RTOS shall implement priority ceiling protocols to limit the extent of priority elevation during priority inheritance.
<<<
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?


[REQUIREMENT]
UID: ZEP-MUTEX-16
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Error Handling
STATEMENT: >>>
When attempting to lock an uninitialized mutex the Zephyr RTOS shall emit an
error.
<<<

[REQUIREMENT]
UID: ZEP-MUTEX-17
STATUS: Draft
TYPE: Functional
COMPONENT: Mutex
TITLE: Mutex Ownership - Unlock Error
STATEMENT: >>>
When attempting to unlock a mutex not owned by the calling thread, the Zephyr RTOS shall emit an error.
<<<

[/SECTION]
Expand Down