The truth about Git

Properties

---

After the git internals and some operations were modeled, we checked for some properties. These properties are important to prove the correct behavior of the model. Such properties were checked using Alloy Analyzer, which tries to find counter examples for the properties. This analysis is bounded, which means that it is not a complete analysis, but instead it analyses the model up to 'n' objects.

Invariant Preservation

An invariant is a property that is always true in the model. In this section, we show that the operations we modeled preserve an invariant when they are performed. Our invariant says the following:

• There is a commit if and only if there is some created branch and HEAD is known;

• The HEAD identifies an existing branch;

• Every branch points to a commit;

• Each branch identifies only and only one commit;

• There is not any object that does not descend from an existing commit;

• Every Tree has content (Blob and Trees) and these objects exists in the repository;

• Every commit object points to an existing tree and if it has a parent it exists in the repository;

• There are not two consecutive commits pointing to the same tree.

Most of these properties are trivial. The first property holds because before the first commit is created it is not possible to create branches, and after that it is never possible to remove the branch identified by HEAD. The property number 6 holds because git does not allow empty Trees and every object contained in a tree exists in the repository. The last property guarantees that each existing commit has a different snapshot from its parent.

To check if an operation preserves an invariant, that invariant must be valid after the operation is performed, assuming that is valid before. We have checked for each operation and we conclude that our operations preserve the invariant.

Idempotent Operations

An operation is said idempotent if after being performed, repeating it does not change the state of the system. It does not make sense to check if this property holds for some operations. For example after removing a file or a branch, it cannot be removed again. The idempotent operations in our model are: commit, add, and checkout. Next we try to justify such property.

The commit operation is idempotent because, if we perform a commit which is equal to the previous, git will not create a new commit and nothing is changed in the repository.

The add operation is also idempotent because while the file in the working directory keeps its content the add operation, after performed the first time, does not brings any differences.

The last operation we proved to be idempotent and maybe the less intuitive is the checkout. As we have seen in Checkout section, the checkout operation updates the index and the working directory to reflect the commit pointed by the branch being checked out. Even if there are some ''weird'' pre-conditions this operation is still idempotent.

Add, Remove and Commit Operations

For this operations we have checked the following properties, which were valid. Notice that when we write ''new file'', we mean a file that does not exists in index.

• Adding a new file to the index and removing it, brings us to the initial state;

• If a commit is performed after an add operation, the added file with the respective content will be in the commit pointed by the branch identified by HEAD;

• If a commit is performed after an remove operation, the removed file will not be present in the commit pointed by the branch identified by HEAD;

• If a commit is performed, a new file is added to index and a new commit is performed, then the first commit and the second commit will point to different Trees;

• Assuming that the invariant is verified and the following operations are performed: commit, add a new file, commit, remove the file added previously, and commit, then the first commit created and the last one will point to the same Tree object;

Branch and Checkout Operations

For the branch operations (add and remove) we have checked two properties. We have checked if after creating a branch and then removing it we reach a state with the same branches as in the begin. We have also checked if when a branch is created it points to the same commit as the branch identified by HEAD. In both cases no counter examples were found.

Relatively to the checkout operation it was verified the following:

• If when the invariant is true and a checkout from a branch ''b'' is performed, then all content from the commit pointed by ''b'' will be in index. Such property is not true, due, the strange pre-condition we described in Checkout section. As it is shown next, if the checkout operation is performed exactly after a commit, the property holds.

• If a commit is performed, a checkout from a random branch is performed and after that a new checkout from the initial branch is also performed, then the index content after the commit will be the same as in the end.