add queue v4 model for spin #26994

kruall · 2025-10-16T11:21:18Z

Changelog entry

...

Description for reviewers

...

github-actions · 2025-10-16T11:21:54Z

🔴 2025-10-16 11:21:53 UTC The validation of the Pull Request description has failed. Please update the description.

Only one category can be selected at a time.

github-actions · 2025-10-16T11:23:19Z

⚪ 2025-10-16 11:23:19 UTC Pre-commit check linux-x86_64-relwithdebinfo for 12bceb2 has started.
⚪ 2025-10-16 11:23:33 UTC Artifacts will be uploaded here
⚪ 2025-10-16 11:26:07 UTC ya make is running...
🟢 2025-10-16 11:26:13 UTC Tests successful.

Ya make output | Test bloat

TESTS	PASSED	ERRORS	FAILED	SKIPPED	MUTED^?
0	0	0	0	0	0

🟢 2025-10-16 11:26:16 UTC Build successful.

github-actions · 2025-10-16T11:23:41Z

⚪ 2025-10-16 11:23:41 UTC Pre-commit check linux-x86_64-release-asan for 12bceb2 has started.
⚪ 2025-10-16 11:23:54 UTC Artifacts will be uploaded here
⚪ 2025-10-16 11:26:29 UTC ya make is running...
🟢 2025-10-16 11:26:35 UTC Tests successful.

Ya make output | Test bloat

TESTS	PASSED	ERRORS	FAILED	SKIPPED	MUTED^?
0	0	0	0	0	0

🟢 2025-10-16 11:26:38 UTC Build successful.

Copilot

Pull Request Overview

Adds new SPIN/Promela models for the “queue v4” design and removes the older “fast” model. Also includes a checked-in SPIN verification result.

Introduces queue_v4_model.pml and queue_v4_model_v2.pml Promela models for producers/consumers with overtaken-slot handling.
Removes legacy queue_fast_model.pml.
Commits a SPIN run output (.result) for queue_v4_model_v2.

Reviewed Changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 10 comments.

File	Description
ydb/library/actors/queues/spin/queue_v4_model_v2.pml	New Promela model variant (v2) for the queue with explicit overtaken path and instrumentation.
ydb/library/actors/queues/spin/queue_v4_model.pml	New Promela model for queue v4 using CAS-style helpers and multiple LTL properties.
ydb/library/actors/queues/spin/queue_v4_model_v2.result	SPIN verification output for the v2 model; appears to be a generated artifact.
ydb/library/actors/queues/spin/queue_fast_model.pml	Removed legacy/alternative queue model.

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

Copilot · 2025-10-16T11:25:12Z

ydb/library/actors/queues/spin/queue_v4_model_v2.pml

+            :: else ->
+                printf("Producer %d: internal channel full, retry later\n", id);
+                planned_pushed_elements = planned_pushed_elements + 1;
+                overflow = true


Missing semicolon after assignment causes a Promela parse error. Add a semicolon.

Suggested change

overflow = true

overflow = true;

Copilot · 2025-10-16T11:25:12Z

ydb/library/actors/queues/spin/queue_v4_model.pml

+            :: else ->
+                printf("Producer %d: internal channel full, retry later\n", id);
+                planned_pushed_elements = planned_pushed_elements + 1;
+                overflow = true


Missing semicolon after assignment causes a Promela parse error. Add a semicolon.

Suggested change

overflow = true

overflow = true;

Copilot · 2025-10-16T11:25:13Z

ydb/library/actors/queues/spin/queue_v4_model.pml

+bool overflow = false;
+Slot buffer[QUEUE_SIZE];
+bool write_seen[ELEMENTS] = {false, false, false};
+bool read_seen[ELEMENTS] = {false, false, false};


Initializer length (3) does not match ELEMENTS (2). This will miscompile or behave incorrectly when ELEMENTS != 3. Either drop the initializer (default is 0/false) or match it to ELEMENTS (e.g., {false, false} for ELEMENTS=2), or initialize in init with a loop.

Suggested change

bool read_seen[ELEMENTS] = {false, false, false};

bool read_seen[ELEMENTS] = {false, false};

Copilot · 2025-10-16T11:25:13Z

ydb/library/actors/queues/spin/queue_v4_model_v2.pml

+bool write_seen[ELEMENTS] = {false, false, false};
+bool read_seen[ELEMENTS] = {false, false, false};


[nitpick] Hard-coding three initializers ties the model to ELEMENTS=3 and undermines parameterization. Consider removing the initializer (arrays default to 0) or initializing in init to keep the model configurable by ELEMENTS.

Suggested change

bool write_seen[ELEMENTS] = {false, false, false};

bool read_seen[ELEMENTS] = {false, false, false};

bool write_seen[ELEMENTS];

bool read_seen[ELEMENTS];

Copilot · 2025-10-16T11:25:13Z

ydb/library/actors/queues/spin/queue_v4_model_v2.pml

+            printf("Consumer %d: get current_head=%d head=%d\n", id, current_head, head);
+            // Implements: ui64 slotIdx = ConvertIdx(currentHead);
+            slot_idx = current_head % QUEUE_SIZE;
+            printf("Consumer %d: get expected=%d for slot_idx=%d slot_value=%d\n", id, expected, slot_idx, buffer[slot_idx].value);


Variable 'expected' is printed before it is assigned in this path, leading to use of an uninitialized value. Initialize 'expected' (e.g., expected = buffer[slot_idx].state;) before printing, or print buffer[slot_idx].state directly.

Suggested change

printf("Consumer %d: get expected=%d for slot_idx=%d slot_value=%d\n", id, expected, slot_idx, buffer[slot_idx].value);

printf("Consumer %d: get state=%d for slot_idx=%d slot_value=%d\n", id, buffer[slot_idx].state, slot_idx, buffer[slot_idx].value);

Copilot · 2025-10-16T11:25:13Z

ydb/library/actors/queues/spin/queue_v4_model_v2.pml

+                    printf("Producer %d: make slot less overtaken slot_idx=%d overtaken_value=%d\n", id, slot_idx, buffer[slot_idx].value);
+
+                :: else ->
+                    printf("Producer %d: INCORRECT STATE\n", id, slot_idx);


Format string has one placeholder but two arguments are passed. Either remove the extra argument or include it in the message, e.g., printf("Producer %d: INCORRECT STATE at slot %d\n", id, slot_idx);

Suggested change

printf("Producer %d: INCORRECT STATE\n", id, slot_idx);

printf("Producer %d: INCORRECT STATE at slot %d\n", id, slot_idx);

Copilot · 2025-10-16T11:25:14Z

ydb/library/actors/queues/spin/queue_v4_model.pml

+    [] (write_seen[0] -> <>(read_seen[0])) &&
+    [] (write_seen[1] -> <>(read_seen[1])) &&
+    [] (write_seen[2] -> <>(read_seen[2])) &&


This LTL references index 2 while ELEMENTS=2 (valid indices are 0 and 1). Either increase ELEMENTS to 3 for this spec, guard these clauses under a preprocessor condition, or parametrize the property to the configured ELEMENTS.

Copilot · 2025-10-16T11:25:14Z

ydb/library/actors/queues/spin/queue_v4_model.pml

+    <> (write_seen[0]) && <> (write_seen[1]) &&
+    [] (write_seen[0] -> []write_seen[0]) &&
+    [] (write_seen[1] -> []write_seen[1]) &&
+    [] (write_seen[2] -> []write_seen[2]) &&


Out-of-bounds access in LTL for ELEMENTS=2. Remove or conditionalize this clause or adjust ELEMENTS.

Copilot · 2025-10-16T11:25:14Z

ydb/library/actors/queues/spin/queue_v4_model.pml

+    <> (read_seen[0]) && <> (read_seen[1]) &&
+    [] (read_seen[0] -> []read_seen[0]) &&
+    [] (read_seen[1] -> []read_seen[1]) &&
+    [] (read_seen[2] -> []read_seen[2]) &&


Out-of-bounds access in LTL for ELEMENTS=2. Remove or conditionalize this clause or adjust ELEMENTS.

Copilot · 2025-10-16T11:25:14Z

ydb/library/actors/queues/spin/queue_v4_model_v2.result

@@ -0,0 +1,39 @@
+(Spin Version 6.4.9 -- 17 December 2018)


[nitpick] This appears to be generated SPIN output; committing volatile result files (with environment-dependent stats) hurts diffs and reproducibility. Consider excluding .result artifacts from version control (e.g., via .gitignore) and, if needed, keep a summarized note in documentation instead.

add queue v4 model

14c4e7d

kruall requested a review from Copilot October 16, 2025 11:21

kruall added the area/actorsystem Actor System related issues label Oct 16, 2025

github-actions bot added the new-feature label Oct 16, 2025

Copilot AI reviewed Oct 16, 2025

View reviewed changes

	bool read_seen[ELEMENTS] = {false, false, false};
	bool read_seen[ELEMENTS] = {false, false};

		bool write_seen[ELEMENTS] = {false, false, false};
		bool read_seen[ELEMENTS] = {false, false, false};

	printf("Consumer %d: get expected=%d for slot_idx=%d slot_value=%d\n", id, expected, slot_idx, buffer[slot_idx].value);
	printf("Consumer %d: get state=%d for slot_idx=%d slot_value=%d\n", id, buffer[slot_idx].state, slot_idx, buffer[slot_idx].value);

	printf("Producer %d: INCORRECT STATE\n", id, slot_idx);
	printf("Producer %d: INCORRECT STATE at slot %d\n", id, slot_idx);

add queue v4 model for spin #26994

Are you sure you want to change the base?

add queue v4 model for spin #26994

Conversation

kruall commented Oct 16, 2025

Changelog entry

Changelog category

Description for reviewers

Uh oh!

github-actions bot commented Oct 16, 2025

Uh oh!

github-actions bot commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions bot commented Oct 16, 2025 •

edited

Loading

github-actions bot commented Oct 16, 2025 •

edited

Loading