deepseek-ai/3FS
1
0
Fork 0
mirror of https://github.com/deepseek-ai/3FS.git synced 2026-11-05 00:47:47 +00:00
Code Issues 166 Projects Packages Wiki Activity

[GH-ISSUE #162] [Spec] Possible Specification Violation #94

New issue
Open
opened 2026-10-26 09:45:01 +00:00 by bsakaguchi · 0 comments
bsakaguchi commented 2026-10-26 09:45:01 +00:00
Owner
Copy link

Originally created by @ChristineZh0u on GitHub (Mar 12, 2025).
Original GitHub issue: https://github.com/deepseek-ai/3FS/issues/162

Originally assigned to: @wlxiong on GitHub.

Hi, I ran checks the P models and found a spec violation in model DataStorage, test case tcThreeClientsWriteNoFailure.
The violation error is: Assertion Failed: PSrc/StorageService.p:2169:9 ChunkReplica(30): writeOp.offset:4 + writeOp.length:2 < sizeof(content):0. It only happens on checks that are using unfair strategy where some transitions or processes are always blocked.

I have attached the output folder to this issue. You can reproduce the spec violation with the commands here.

BugFinding_DataStorage_ tcThreeClientsWriteNoFailure.zip

Originally created by @ChristineZh0u on GitHub (Mar 12, 2025). Original GitHub issue: https://github.com/deepseek-ai/3FS/issues/162 Originally assigned to: @wlxiong on GitHub. Hi, I ran checks the P models and found a spec violation in model `DataStorage`, test case `tcThreeClientsWriteNoFailure`. The violation error is: `Assertion Failed: PSrc/StorageService.p:2169:9 ChunkReplica(30): writeOp.offset:4 + writeOp.length:2 < sizeof(content):0`. It only happens on checks that are using unfair strategy where some transitions or processes are always blocked. I have attached the output folder to this issue. You can reproduce the spec violation with the commands [here](https://p-org.github.io/P/old/advanced/debuggingerror/?h=schedu#replaying-the-error-schedule). [BugFinding_DataStorage_ tcThreeClientsWriteNoFailure.zip](https://github.com/user-attachments/files/19216000/BugFinding_DataStorage_.tcThreeClientsWriteNoFailure.zip)
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
SF-Zhou-patch-1
No results found.
Labels
Clear labels   
pull-request
Mirrored from GitHub Pull Request

No labels
pull-request
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
deepseek-ai/3FS#94
No description provided.