git-annex/doc/todo/proving_preferred_content_behavior.mdwn
Joey Hess 969e6c2747
sped up sim step by about 200%
Noticed that it was quite slow compared with things like action
sendwanted. Guessed that the slowdown is largely due to every step
doing a simulated git pull/push.

So, rather than always doing a pull/push, only do those when no actions
are found without doing a pull/push.

This does mean that step will sometimes experience a split brain
situation, but that seems like a good thing? Because step ought to
explore as many possible scenarios as it reasonably can.
2024-09-23 15:45:47 -04:00

117 lines
5.1 KiB
Markdown

[[!toc ]]
## motivating examples
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
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.
Mostly, git-annex manages to keep things stable that seem like they would
not be. Consider repo A that is not in group foo, and B is in group foo. A
has preferred content "onlyingroup=foo". This will make A want a file that
is in B. And once it has it, it will not want to drop it. That's because
when dropping, it considers if it would be preferred content after the
drop. In this case it would, so it doesn't drop it.
## 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 `fullybalanced()` is not stable when used
on its own, and so `balanced()` adds an "or present" to stabilize it.
And so `not balanced()` includes `not present`, which is bad!
## 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`.
> This is now detected and such an unstable expression never matches.
> --debug explains why too.
>
> Note that the detection will not be trigged by `"not (not present)"`,
> but it will by `"include=* or (not present)"` even though that is always
> stable, because `"include=*"` always matches and so what it's ORed with
> doesn't matter. Probably noone will set something like that in real life
> though.
>
> It's problimatic to make `git-annex wanted` warn about it. Consider
> if in one repository, groupwanted is set to "present". In another
> repository, which is disconnected, wanted is set to "not groupwanted".
> Both operations are ok, but upon merging the two repositories,
> the combined effect is that "not present" has been set.
>
> So while it could warn sometimes on setting "not present",
> it would sometimes not be able to. Better to not warn inconsistently.
> --[[Joey]]
## simulation
Simulation seems fairly straightforward, just simulate the network of
git-annex repositories with random files with different sizes and
metadata. Or use the current files 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.
The sim could be run in a clone of a repository, and update location
logs as it runs. This would let the user query with `whereis` and
`maxsize` etc to see what happens.
Such a repository's location tracking would no longer match reality,
so it would need to be clearly marked as a simulation result, and be
prevented from merging back into another repository. This can be done by
adding a new Difference to the repository.
The sim would need a map of repositories with connections between them.
Perhaps `git-annex map` could be used?
For each step of the sim, it would pick a repository from the map
(excluding special remotes), and simulate an operation being run in that
repository, affecting it and its remotes.
Split brain needs to be simulated, so the operations in the sim should
include pushing and fetching the git-annex branch. The ref of each
git-annex branch of each repository would be stored, with
refs/heads/git-annex being set to the git-annex branch of the repository
it is currently simulating an operation in.
The other operations would include get, drop, copy, move, sync, all
with preferred content respected.
May want to also simulate adding files to a repository, which would be
generated (without any actual content) according to simulation parameters.
Also file moves and deletions. `git-annex fuzztest` has some prior art.
The location log history could be examined at the end of the simulation
to find problems like instability.
[[!tag projects/openneuro]]
> [[done]], see `git-annex sim` command. --[[Joey]]