Trace existing mutex and semaphore tests to KRN-SYNC-012, -013, -023, -025, -026, -028

Open
#115 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
55/100
Issue type
Feature
Clarity
Mostly clear
Activity status
Active
Tech stack
c
Domain
testing

Research direction

Read the Statement and Verification lines for the six requirements in docs/requirements/KRN-SYNC.md, then inspect tests/conformance/test_mutex.c and the existing semaphore cases for their EMB_TEST_REQ citations. Trace each behavior to its case and add requirement IDs only where the case verifies the statement; identify any uncovered behavior in the PR. Build and run native-gcc, collect evidence with tools/evidence/collect.py, and verify the matrix with tools/evidence/matrix.py.

Written by the indexing model from the issue text.

Description

good first issue

Goal

Several mutex and semaphore requirements show no executed test in the requirement matrix, although tests for those behaviours exist. The tests cite other requirement IDs. Find which existing cases check each requirement, cite it, and add a case where none does.

This is a good way to learn how the project ties requirements to tests.

The requirements

From docs/requirements/KRN-SYNC.md:

  • KRN-SYNC-012 ceiling protocol on the same object type
  • KRN-SYNC-013 recursive locking is an option
  • KRN-SYNC-023 recursion and self-relock
  • KRN-SYNC-025 owner death policies
  • KRN-SYNC-026 ceiling rules
  • KRN-SYNC-028 semaphore semantics

For example, mutex_recursive_counts in tests/conformance/test_mutex.c checks recursion but cites only KRN-SYNC-004. mutex_owner_death_policy cites KRN-SYNC-011, not -025.

How a case cites a requirement

Inside a case, EMB_TEST_REQ("KRN-SYNC-004", ...). A run prints one CASE ... req=... line per case, and tools/evidence/matrix.py builds the matrix from them (case evidence).

Steps

  1. For each requirement, read its Statement and Verification lines.

  2. Find the cases that check what the statement says, and add the ID to their EMB_TEST_REQ. Cite only what the case really checks.

  3. Where no case checks part of a statement, write the case, or list what is missing in the PR.

  4. Build and run native-gcc (see the README's quick start). Then collect the run's evidence and build the matrix:

    python3 -I tools/evidence/collect.py --build build/native-gcc --preset native-gcc --out native-gcc.json
    python3 -I tools/evidence/matrix.py native-gcc.json --baseline tools/evidence/baseline.json
    

Done when

  • The PR names, for each of the six requirements, the cases that now cite it, or why none can yet.
  • CI's evidence job passes. It will report the newly evidenced pairs.
Dominant language
C
Stars
1
Forks
1
Avg merge
14h 21m
Merged PRs (30d)
125

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from EmbLinkOs/EmbLinkRTOS

All issues in EmbLinkOs/EmbLinkRTOS

Similar issues

More C issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.