Solving Concurrency Bugs Using Schedules and Imagination
ankush.dev
ankush.dev
Generally speaking though: yes, writing it down can help A LOT, and starting with what you can see is one of those obvious-in-retrospect things that are easily forgotten when under pressure. There are often a LOT of possibilities, and getting it out of your head so you can enumerate them more precisely can super duper important. Intuition for problematic sequences to check first will come with time.
What the Shuttle library is doing is basically automatically going through all the permutations of the schedule diagrams described int his blog post.
We used it at AWS to verify the custom filesystem we wrote to power AWS S3.
If you're curious, I wrote a little tutorial on it here: https://grantslatton.com/shuttle
No better training than a great spaghetti ball of promise chains.