`txn-list-append` workload fails to detect invalid return for read operations

[aquarhead]

I had a typo in my code which caused all txn_ok response to use "append" for all functions. Such as this:

INFO [2021-04-13 23:32:29,761] jepsen worker 0 - jepsen.util 0	:invoke	:txn	[[:append 224 6] [:r 226 nil] [:r 227 nil] [:r 226 nil]]
INFO [2021-04-13 23:32:29,761] jepsen worker 0 - jepsen.util 0	:ok	:txn	[[:append 224 6] [:append 226 [1 2 3 4 5 6 7 8 9]] [:append 227 [1 2 3 4 5 6 8 9]] [:append 226 [1 2 3 4 5 6 7 8 9]]]

However in this case maelstrom considers the run valid:

INFO [2021-04-13 23:32:29,998] jepsen worker 1 - jepsen.util 1	:invoke	:txn	[[:r 229 nil] [:r 229 nil]]
INFO [2021-04-13 23:32:29,998] jepsen worker 1 - jepsen.util 1	:ok	:txn	[[:append 229 [1 3 5 6]] [:append 229 [1 3 5 6]]]
INFO [2021-04-13 23:32:30,005] jepsen node n1 - maelstrom.db Tearing down n1
INFO [2021-04-13 23:32:30,005] jepsen node n0 - maelstrom.db Tearing down n0
...
 :workload {:valid? true},
 :valid? true}


Everything looks good! ヽ(‘ー`)ノ

I noticed this when I tried a multi-node test when only finished the single node part, so found it weird that I can successfully pass the test. When I fix my typo it now correctly identifies my single node code to fail for multi node test.

It seems this is a deeper issue in Jepsen/Elle? (or intended behaviour?)

[aphyr]

Ah, yeah, this is somewhere we could do more rigorous checking. As far as Jepsen and Elle are concerned your histories were, in fact, correct: append-only histories are always legal, and your system insisted that the transactions it executed were append-only! This generally doesn't come up in Jepsen testing because we control the transaction generation, but in Maelstrom we're blindly trusting whatever the node happens to return, and that's clearly not correct. I'd welcome a patch to either Maelstrom or Elle which validates that completion transactions are compatible with their invocations!

[aquarhead]

Thanks for clarifying, I had a rough understanding of this history concept. I'm not entirely sure what should be considered as "compatible" though - does each µ-op must return in same order? or does it allow reordering but each µ-op need to present? or does it allow multiple µ-op to map to a single one in request? (e.g. multiple read response for a single read request)

For example for this input [[:append 224 6] [:r 226 nil]], which ones of the following should be considered as valid?

1. [[:append 224 6] [:r 226 [1]]] - exact order (can be checked by comparing array of function + key)
2. [[:r 226 [1]] [:append 224 6]] - reordered but all µ-ops exist (check with set of function + key)
3. [[:append 224 6] [:r 226 [1]] [:r 226 [1 2]]] - multiple read responses (check function + key count?)

(I haven't finished the entire Datomic chapter so might be a dumb question)

[aphyr]

Only option 1 is valid there. You want precise equality except for read values, which should be null in the invoke. :-)

[aquarhead]

BTW I opened a PR ^ for this in case you missed it :D