I’m trying to model a storage system which is composed of multiple shards. Any file uploaded will be placed in one of these shards. This system supports versioning, which means subsequent uploads of a file end up in the same shard as the first upload.
I’m trying to model this system where I’d like to see 2 or more concurrent uploads occur, in one of its possible behaviors given by the following model.
sig File {
var loc : set Shard
}
sig Shard {}
pred upload[f: File] {
some f.loc implies loc' = loc
else (some s: Shard| loc' = loc + f->s)
}
pred stutter {
loc' = loc
}
pred init {
no loc
}
check file_exists_in_atmost_one_shard {
all f: File | lone f.loc
}
fact transitions {
init
always (
(some f: File| upload[f]) or
stutter
)
}
run show {} for 5
I expect some f expression in the transitions fact is satisfied by more than one File in a single step of the behavior. For some reason I’m unable to coax the visualizer to show such a trace. I even tried modifying the transitions fact to have, some f: File | upload[f] and upload[f]. Clearly, I’m missing something in my understanding of Alloy.
In the upload predicate, I wish to specify that if a file is already in one of the shards, then the upload will pick the same shard, so the loc relation is unmodified. Otherwise, it would pick a shard at random and loc is updated accordingly.
My goal is to demonstrate that 2 or more concurrent uploads can see loc as empty and proceed to add 2 different Shards to the loc relation. In the real world, a file’s versions may be placed in different shards.
Usually, we do not model “true” concurrency (things happening at the same time), but concurrency is modelled by interleaving: the “concurrent” execution of action A and B is specified by allowing both traces where B happens immediately after A and vice-versa.
That model of concurrency is what fact transitions is enforcing in your case. On first sight, constraint some f : File | upload[f] seems to suggests that we can have more than one “truly” concurrent uploads, but that is not possible due to the way the effect on loc is specified in predicate upload: note that constraint loc' = loc + f->s cannot be true for two different files at the same time.
In this interleaved model, if you want to see two concurrent uploads you should ask for a trace where one happens after the other, for example using the following command.
run show {
some disj f,g : File | upload[f] and after upload[g]
} for 5
You can also model “true” concurrency in Alloy, if that is what you really want, but it is not very standard to do so, nor trivial.
Btw, in your check you are missing a always: as is you are only checking that in the initial state all files have at most one shard associated, which is trivially true due to the initial state constraint.
Thank you for explaining the problem in my approach. This made me realize that I was oversimplifying the behavior (or problematic behavior) I was trying to model. I have taken another shot at this.
Facts about the system:
Files can have one or more versions.
Each version of a file is located in a Shard.
Behavior:
Multiple client programs can upload a file (identified by name) concurrently.
Each client upload corresponds to a file version, e.g. (F1, V1).
The ‘server’ program tries to store versions of a file on the same Shard as the first version of a file.
When 2 or more client uploads of a file with no versions occur concurrently, the server fails to uphold this property.
This behavior is captured by the run command concurrent_writes.
Modeling notes
upload predicate takes s: Shard as an argument to control the shard selection when the file being uploaded has no versions stored yet. This has been used in the run command concurrent_writes.
process_upload predicate separates the shard selection and actual storing of a file version to its shard to allow for more ‘interesting’ interleaving of events.
TL;DR: I was successful in modeling the behavior I wanted to via the run command. This gives me confidence that my spec is consistent (to a point).
Is the following spec modeling concurrency more idiomatically (to Alloy) than my previous attempt?
Context: I’ve a few sub-systems at work that I’d like to model using Alloy, initially to document them, and eventually to use them for future development.
sig File {
, var versions : set Version
, var inflight: Version -> Shard // uncommitted versions
}
sig Version{}
sig Shard {
var fileVersions : File -> Version
}
// upload represents the ‘client’ action of a file version upload.
// Shard s is passed as a recommendation and applies only
// until f has no ‘committed’ versions.
pred upload [f: File, v: Version, s: Shard] {
v not in (f.versions + f.inflight.Shard)
no fileVersions.(f.versions).f
implies (inflight' = inflight + f->v->s)
else (some s: fileVersions.(f.versions).f| inflight' = inflight + f->v->s)
fileVersions' = fileVersions
versions' = versions
}
// process_upload writes a version to a shard picked at the time of upload.
pred process_upload[f: File, v: Version] {
let s = f.inflight[v] {
inflight’ = inflight - f->v->s
fileVersions’ = fileVersions + s->f->v
versions’ = versions + f->v
}
}
pred stutter {
versions’= versions
fileVersions’ = fileVersions
inflight’ = inflight
}
pred init {
no versions
no fileVersions
no inflight
}
fact transitions {
init
always (
(some f: File, v: Version, s: Shard| upload[f, v, s]) or
(some f: File, v: Version| process_upload[f, v]) or
stutter)
}
run concurrent_writes {
some f: File, disj v1, v2: Version, disj s1, s2: Shard {
upload[f, v1, s1]; upload[f, v2, s2]; process_upload[f, v1]; process_upload[f, v2]
}
} for 5 but exactly 2 File, exactly 2 Version, exactly 2 Shard
If you feel the Shard argument to upload is a bit unnatural, you could also specify the upload action as follows.
pred upload [f: File, v: Version] {
v not in (f.versions + f.inflight.Shard)
no fileVersions.(f.versions).f
implies (some s : Shard | inflight' = inflight + f->v->s)
else (some s: fileVersions.(f.versions).f| inflight' = inflight + f->v->s)
fileVersions' = fileVersions
versions' = versions
}
You would have to adapt the run command accordingly, ofc. And, to explore different upload possibilities (same shard or different shard), you would need to use the New Fork button in the second transition.
Thank you for simplifying the upload predicate. Now the model looks very readable to me.
I wanted to test some properties via the check command on this model. I added the following check
check versions_invariant {
some f: File, v: Version {
always (v in f.versions => once upload[f, v])
}
}
This failed with a counter example containing a single File atom and single Shard atom. I’m confused (again). Following are the reasons for my confusion.
some f: File, v: Version in the check command should guarantee that the assertion must be checked only for those behaviors that have at least one File atom and one Version atom.
I expected the antecedent of the implies to be true in the counter example. i.e the counter example should have contained a non-empty versions relation with some f and v related as specified. This wasn’t the case either.
Clearly, I’m missing something. Any pointers would be helpful.
No, that is not what is being checked. You are checking if in all possible instances of your model there exists some File and some Version such that something is true (the property inside the existential quantifier doesn’t actually matter). This is obviously false, as the counterexample showed (it is an instance without versions, which I guess is allowed by your fact). I think that you want to replace the some quantifier by a all quantifier, because you want to check the inner property for all files and versions that may exist. If none exists, the universal all quantifier will be trivially true, so you don’t need to restrict the verification to instances where there are at least one File and at least one Version.
As I mentioned, the assertion failed because of the outermost quantifier. Since there are no versions in the counterexample the property is trivially false, and it not longer matters what is the value of the inner property.
Thank you again for pointing out the gap in my understanding. Changing some to all did the trick. More importantly, I understand why now.
I was facing another problem while I was trying to wrap my head around this earlier. This is to do with how let binding works.
I had another run command to help me ‘debug’ my model. It goes like this,
run show {
some versions
}
The expectation was to see the examples generated and verify that all of them had versions relation and fileVersions relation filled such that the transitions fact was honored. To my surprise, there were examples where the versions relation alone was populated while other mutable relations remained empty, violating the transitions fact.
In a desperate attempt, I changed the process_upload predicate from,
pred process_upload[f: File, v: Version] {
let s = f.inflight[v] {
inflight’ = inflight - f->v->s
fileVersions’ = fileVersions + s->f->v
versions’ = versions + f->v
}
}
I recognize the problem with the following predicate now.
pred process_upload[f: File, v: Version] {
let s = f.inflight[v] {
inflight’ = inflight - f->v->s
fileVersions’ = fileVersions + s->f->v
versions’ = versions + f->v
}
}
The let expression simply binds s to the value of the expression. s could evaluate to either a non-empty or an empty set. When it evaluates to none, f->v mapping would be added to the versions violating the intended of invariant of, a Version can be added to the set of versions of a File iff it was placed in a Shard (i.e persisted).
That explains why the run command showed an example with non-empty versions relation while others were empty.