Published 2022-10-09T14:30:00.002Z by Physics Derivation Graph
The Physics Derivation Graph is just a CRUD application, so I didn't expect TLA+ would be relevant. My initial view was that there isn't an algorithm or a protocol in the PDG. The PDG is just a webpage, some middleware (e.g., bash or Python) and a back-end database (CSV, SQL, JSON, Neo4j, etc). Standard MVC applies.
After spending 1 day reviewing TLA+ materials, I realized the PDG has a workflow specification that I hadn't previously considered in detail.
User has a derivation in mind and they want to integrate it with existing PDG content. User knows their derivation's expressions, steps, symbols (variables and constants), and operators.
User writes their derivation into the PDG referencing existing symbols, existing expressions, and existing inference rules.
If the relevant symbol isn't available, add it.
If an existing symbol needs to be corrected/revised/merged, modify it.
If the relevant inference rule isn't available, add it.
If an existing inference rule needs to be corrected/revised/merged, modify it.
Integrated derivation steps are checked for correctness using a Computer Algebra System (e.g., SymPy, Mathematica, etc)
That user story sounds reasonable until you consider two concurrent users editing the same steps or expressions or symbols or inference rules or operators. If each of the above steps are considered atomic, there are potential conflicts.
One user could be attempting to create a new derivation step while another modifies existing symbols or inference rules.
Two users could concurrently attempt to modify/merge/edit existing symbols or inference rules. When they commit their change, the thing they are changing may have disappeared or been altered.
One way to avoid the above potential for conflict would be to lock the database while edits are made (no concurrent users). Another avoidance mechanism would be to queue changes and check consistency of every change sequentially (serialize concurrency).