From 7044232696af7c0f5e4d85836d2aa6f9bd9f15e5 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Wed, 13 Mar 2024 11:04:06 -0400 Subject: [PATCH] todo --- .../proving_preferred_content_behavior.mdwn | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 doc/todo/proving_preferred_content_behavior.mdwn diff --git a/doc/todo/proving_preferred_content_behavior.mdwn b/doc/todo/proving_preferred_content_behavior.mdwn new file mode 100644 index 0000000000..73f181bc0d --- /dev/null +++ b/doc/todo/proving_preferred_content_behavior.mdwn @@ -0,0 +1,75 @@ +Preferred content expressions can be complicated to write and reason about. +A complex expression can involve lots of repositories that can get into +different states, and needs to be written to avoid unwanted behavior. + +It would be very handy to provide some way to prove things about behavior +of preferred content expressions, or a way to simulate the behavior of a +network of git-annex repositories with a given preferred content configuration + +## motivating examples + +For example, consider two reposities A and B. A is in group M and B is in +group N. A has preferred content `not inallgroup=N` and B has `not inallgroup=M`. + +If A contains a file, then B will want to also get a copy. And things +stabilize there. But if the file is removed from A, then B also wants to +remove it. And once B has removed it, A wants a copy of it. And then B also +wants a copy of it. So the result is that the file got transferred twice, +to end up right back where we started. + +The worst case of this is `not present`, where the file gets dropped and +transferred over and over again. The docs warn against using that one. But +they can't warn about every bad preferred content expression. + +## balanced preferred content + +When [[design/balanced_preferred_content]] is added, a whole new level of +complexity will exist in preferred content expressions, because now an +expression does not make a file be wanted by a single repository, but +shards the files amoung repositories in a group. + +And up until this point preferred content expressions have behaved the same no +matter the sizes of the underlying repositories, but balanced preferred +content does take repository fullness into account, which further +complicates fully understanding the behavior. + +Notice that `balanced()` (in the current design) is not stable when used +on its own, and has to be used as part of a larger expression to make it +stable, eg: + + ((balanced(backup) and not (copies=backup:1)) or present + +So perhaps `balanced()` should include the other checks in it, +to avoid the user shooting themselves in the foot. On the other +hand, if `balanced()` implicitly contains `present`, then `not balanced()` +would include `not present`, which is bad! + +(For that matter, what does `not balanced()` even do currently?) + +## proof + +What could be proved about a preferred content expression? + +No idea really. Would be interesting to consider what formal methods can +do here. Could a SAT solver be used somehow for example? + +## static analysis + +Clearly `not present` is an problematic preferred content expression. It +would be good if git-annex warned and/or refused to set such an expression +if it could detect it. Similarly `not groupwanted` could be detected as a +problem when the group's preferred content expression contains `present`. + +Is there is a more general purpose and not expensive way to detect such +problematic expressions, that can find problems such as the +`not inallgroup=N` example above? + +## simulation + +Simulation seems fairly straightforward, just simulate the network of +git-annex repositories with random files with different sizes and +metadata. Be sure to enforce invariants like numcopies the same as +git-annex does. + +Since users can write preferred content expressions, this should be +targeted at being used by end users. -- 2.30.2