Thanks for the answers, I appreciate that.
If you have time, I have another round of questions:
1. Did you try formal methods like TLA+ on the client? I think that the logic covered by CanopyCheck may be a nice target.
2. Do you have some tests with several clients running at the same time on a shared directory? In particular, I think of the termination invariant where the clients are fighting because several users have reorganized the directory by moving a lot of stuff, and each client is trying to converge in a different direction (ie they are making operations that cancelled the ones made by other clients).
3. The article says "In the Nucleus data model, nodes are represented by a unique identifier". Does it happen that a node has to change its identifier? For example, in a scenario like this one:
(ada) $ offline
(grace) $ offline
(grace) $ mv ~/Dropbox/shared/TODO.txt ~/Dropbox/private-grace/
(ada) $ mv ~/Dropbox/shared/TODO.txt ~/Dropbox/private-ada/
(ada) $ echo 'foo' >> ~/Dropbox/private-ada/TODO.txt
(grace) $ echo 'bar' >> ~/Dropbox/private-grace/TODO.txt
(ada) $ online
(grace) $ online
If you have time, I have another round of questions:
1. Did you try formal methods like TLA+ on the client? I think that the logic covered by CanopyCheck may be a nice target.
2. Do you have some tests with several clients running at the same time on a shared directory? In particular, I think of the termination invariant where the clients are fighting because several users have reorganized the directory by moving a lot of stuff, and each client is trying to converge in a different direction (ie they are making operations that cancelled the ones made by other clients).
3. The article says "In the Nucleus data model, nodes are represented by a unique identifier". Does it happen that a node has to change its identifier? For example, in a scenario like this one: