tla-plus: to_check doesn't decrease during StageWritesAndRecordLoop

[y-taka-23]

Describe the problem

In StageWritesAndRecordLoop, the committer process picks a key from pipelined to_check set one-by-one, then queries the state of the corresponding intent. Thus, the line:

to_check := to_check \union {key}

should be:

to_check := to_check \ {key}

[blathers-crl]

Hello, I am Blathers. I am here to help you get the issue triaged.

Hoot - a bug! Though bugs are the bane of my existence, rest assured the wretched thing will get the best of care here.

I have CC'd a few people who may be able to assist you:

• @ricardocrdb (member of the technical support engineering team)

If we have not gotten back to your issue within a few business days, you can try the following:

• Join our community slack channel and ask on #cockroachdb.
• Try find someone from here if you know they worked closely on the area and CC them.

_{🦉 Hoot! I am a Blathers, a bot for CockroachDB. My owner is otan.}

[nvanbenschoten]

Hi @y-taka-23, thanks for the report and good spot! That line does look incorrect. Would you like to submit a PR to fix it?

Also, I'd love to hear about how you found this? I stumbled upon https://speakerdeck.com/ytaka23/cloudnative-days-tokyo-2020 on Twitter earlier today and was very impressed.

[y-taka-23]

Would you like to submit a PR to fix it?

Of course yes! I'm going to do within this week.

I'd love to hear about how you found this?

Actually just by chance. For demonstrating TLA+'s semantics, I tried to show "If the committer couldn't fail, ImplicitCommitLeadsToExplicitCommit holds without the recovery procedure". Concretely speaking:

• Make the committer process fair
• Delete the skip clause of "unsuccessful consensus" in PipelineWrites
• Delete the preventers

Against my expectation, TLC reported a violation with QueryPipelinedWrite-StageWritesAndRecordLoop infinite loop.