Skip to content

sync: 11 more ordering issues found by a TLA+ re-run, still reproducing on main (follow-up to #792) #827

Open

Description

@Jakuboola

I turned the #792 approach into a reusable agent skill and tested it blind: the agent got this repo at 2342bba (before #792 was filed), no access to the issue, and a TLA+ model of sync pull/diff/push. It replayed every counterexample as a test through the real SyncService, with only the Storage API faked.

It rediscovered most of #792 (A, B, C, E, F, H, plus G from reading the code) and found more. I re-ran all the tests on current main (2a8134d). The ones below still fail there.

Tests and the TLA+ model, with run instructions: https://gist.github.com/Jakuboola/a07f001b4af82c93fc8a311137ef849c

The fake's server assumptions were checked against a real test project (default branch, us-east4 GCP). A trashed config drops out of the live listing. A second DELETE on a trashed config purges it. PUT has no version check, so the last writer wins. PUT and row POST on a trashed config return 404. POST/PUT responses include configuration.

New

What happens Test
1 Re-created a config after a UI trash, then crash before the manifest save: the re-run creates another copy, even though the new id is already on disk test_a_prime_tracked_recreate_crash_before_save_then_rerun_duplicates
2 Crash after a row POST: the re-run creates a duplicate row (rows have no id on disk) test_b_row_create_crash_before_save_then_rerun_duplicates_row
3 Two sync push at once in one dir: both create the same config; a double DELETE purges it test_c_concurrent_pushes_both_create_same_dir, test_c_concurrent_pushes_double_delete_purges
4 UI edit between push's diff and its PUT is silently overwritten test_d_ui_edit_between_diff_and_put_is_not_overwritten
5 User deletes a dir after someone edited the config in the UI: push trashes it, no conflict test_e_delete_of_ui_edited_config_reports_conflict
6 Config trashed in the UI between push's diff and its DELETE gets purged permanently test_h_ui_trash_between_diff_and_delete_is_not_purged
7 transform.sql edit of a config that push created never shows in sync diff test_J_companion_edit_after_push_create_is_reported
8 Local edit saved while push runs is lost (writeback from pre-read data) or marked as synced test_m_edit_during_put_is_overwritten_by_writeback, test_m_edit_between_writeback_and_stamp_is_not_reported
9 Unparseable _config.yml makes push delete the remote config test_o_unparseable_config_yaml_is_not_deleted_remotely
10 Pull crashes after moving a renamed config's dir: next push creates a copy under a new id and trashes the original test_P_pull_crash_after_rename_then_push_keeps_identity
11 Pull crashes after removing a dir: stale manifest entry. Harmless unless the config is restored in the UI first, then push deletes it again test_R_pull_crash_after_rmtree_leaves_no_stale_entry

Still open from #792

  • E (adopted file, 2-way diff overwrites a UI edit): test_f_adopt_by_id_after_crash_does_not_overwrite_ui_edit
  • F (retry after an aborted or crashed push duplicates): test_a_lost_create_response_then_rerun_creates_duplicate, test_a_crash_after_create_then_rerun_creates_duplicate

Notes

The tests are in the gist as xfail(strict=True). Happy to turn them into a PR (tests plus the model, no production changes, same as #793) if someone can give me access.

Slack thread (internal): https://keboolaglobal.slack.com/archives/C5BPD3T6D/p1791140864898829?thread_ts=1790725090.440759&cid=C5BPD3T6D

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions