[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Experimenting with PlusCal / TLA+ at Dropbox



Hi Stephan,
 
I understand that this issue is not present in the spec that you posted.

I believe the issue was present in the original spec, but the modifications that you made to cas_sentinels fixed it. In the original spec, a writer can proceed with db_commit if cas_error_keys is empty, even if cas_success_keys is not equal to db_write_keys. Such a state can occur if db_write_keys is non-empty and the writer takes a cas_sentinels step when it is Down. This violates consistency because keys can be modified in the database when they are not Pending in the cache.

You fixed this issue by (a) removing cas_error_keys and comparing cas_success_keys to db_write_keys and (b) changing the if-statement in cas_sentinels to an await.

- Dan