From 04a6af4272a46bdd464ad029106c129b26f10b9f Mon Sep 17 00:00:00 2001 From: Santiago Perez De Rosso Date: Mon, 7 Apr 2014 18:04:59 -0400 Subject: [PATCH] alloy support --- lib/linguist/languages.yml | 5 + samples/Alloy/file_system.als | 59 +++++++++ samples/Alloy/marksweepgc.als | 83 +++++++++++++ samples/Alloy/views.als | 217 ++++++++++++++++++++++++++++++++++ 4 files changed, 364 insertions(+) create mode 100644 samples/Alloy/file_system.als create mode 100644 samples/Alloy/marksweepgc.als create mode 100644 samples/Alloy/views.als diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 6eb2a378..212bb733 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -86,6 +86,11 @@ Agda: color: "#467C91" primary_extension: .agda +Alloy: + type: programming # 'modeling' would be more appropiate + color: "#cc5c24" + primary_extension: .als + ApacheConf: type: markup aliases: diff --git a/samples/Alloy/file_system.als b/samples/Alloy/file_system.als new file mode 100644 index 00000000..60fd959b --- /dev/null +++ b/samples/Alloy/file_system.als @@ -0,0 +1,59 @@ +module examples/systems/file_system + +/* + * Model of a generic file system. + */ + +abstract sig Object {} + +sig Name {} + +sig File extends Object {} { some d: Dir | this in d.entries.contents } + +sig Dir extends Object { + entries: set DirEntry, + parent: lone Dir +} { + parent = this.~@contents.~@entries + all e1, e2 : entries | e1.name = e2.name => e1 = e2 + this !in this.^@parent + this != Root => Root in this.^@parent +} + +one sig Root extends Dir {} { no parent } + +lone sig Cur extends Dir {} + +sig DirEntry { + name: Name, + contents: Object +} { + one this.~entries +} + + +/** + * all directories besides root have one parent + */ +pred OneParent_buggyVersion { + all d: Dir - Root | one d.parent +} + +/** + * all directories besides root have one parent + */ +pred OneParent_correctVersion { + all d: Dir - Root | (one d.parent && one contents.d) +} + +/** + * Only files may be linked (that is, have more than one entry) + * That is, all directories are the contents of at most one directory entry + */ +pred NoDirAliases { + all o: Dir | lone o.~contents +} + +check { OneParent_buggyVersion => NoDirAliases } for 5 expect 1 + +check { OneParent_correctVersion => NoDirAliases } for 5 expect 0 diff --git a/samples/Alloy/marksweepgc.als b/samples/Alloy/marksweepgc.als new file mode 100644 index 00000000..b8081e3f --- /dev/null +++ b/samples/Alloy/marksweepgc.als @@ -0,0 +1,83 @@ +module examples/systems/marksweepgc + +/* + * Model of mark and sweep garbage collection. + */ + +// a node in the heap +sig Node {} + +sig HeapState { + left, right : Node -> lone Node, + marked : set Node, + freeList : lone Node +} + +pred clearMarks[hs, hs' : HeapState] { + // clear marked set + no hs'.marked + // left and right fields are unchanged + hs'.left = hs.left + hs'.right = hs.right +} + +/** + * simulate the recursion of the mark() function using transitive closure + */ +fun reachable[hs: HeapState, n: Node] : set Node { + n + n.^(hs.left + hs.right) +} + +pred mark[hs: HeapState, from : Node, hs': HeapState] { + hs'.marked = hs.reachable[from] + hs'.left = hs.left + hs'.right = hs.right +} + +/** + * complete hack to simulate behavior of code to set freeList + */ +pred setFreeList[hs, hs': HeapState] { + // especially hackish + hs'.freeList.*(hs'.left) in (Node - hs.marked) + all n: Node | + (n !in hs.marked) => { + no hs'.right[n] + hs'.left[n] in (hs'.freeList.*(hs'.left)) + n in hs'.freeList.*(hs'.left) + } else { + hs'.left[n] = hs.left[n] + hs'.right[n] = hs.right[n] + } + hs'.marked = hs.marked +} + +pred GC[hs: HeapState, root : Node, hs': HeapState] { + some hs1, hs2: HeapState | + hs.clearMarks[hs1] && hs1.mark[root, hs2] && hs2.setFreeList[hs'] +} + +assert Soundness1 { + all h, h' : HeapState, root : Node | + h.GC[root, h'] => + (all live : h.reachable[root] | { + h'.left[live] = h.left[live] + h'.right[live] = h.right[live] + }) +} + +assert Soundness2 { + all h, h' : HeapState, root : Node | + h.GC[root, h'] => + no h'.reachable[root] & h'.reachable[h'.freeList] +} + +assert Completeness { + all h, h' : HeapState, root : Node | + h.GC[root, h'] => + (Node - h'.reachable[root]) in h'.reachable[h'.freeList] +} + +check Soundness1 for 3 expect 0 +check Soundness2 for 3 expect 0 +check Completeness for 3 expect 0 diff --git a/samples/Alloy/views.als b/samples/Alloy/views.als new file mode 100644 index 00000000..3a5ab82b --- /dev/null +++ b/samples/Alloy/views.als @@ -0,0 +1,217 @@ +module examples/systems/views + +/* + * Model of views in object-oriented programming. + * + * Two object references, called the view and the backing, + * are related by a view mechanism when changes to the + * backing are automatically propagated to the view. Note + * that the state of a view need not be a projection of the + * state of the backing; the keySet method of Map, for + * example, produces two view relationships, and for the + * one in which the map is modified by changes to the key + * set, the value of the new map cannot be determined from + * the key set. Note that in the iterator view mechanism, + * the iterator is by this definition the backing object, + * since changes are propagated from iterator to collection + * and not vice versa. Oddly, a reference may be a view of + * more than one backing: there can be two iterators on the + * same collection, eg. A reference cannot be a view under + * more than one view type. + * + * A reference is made dirty when it is a backing for a view + * with which it is no longer related by the view invariant. + * This usually happens when a view is modified, either + * directly or via another backing. For example, changing a + * collection directly when it has an iterator invalidates + * it, as does changing the collection through one iterator + * when there are others. + * + * More work is needed if we want to model more closely the + * failure of an iterator when its collection is invalidated. + * + * As a terminological convention, when there are two + * complementary view relationships, we will give them types + * t and t'. For example, KeySetView propagates from map to + * set, and KeySetView' propagates from set to map. + * + * author: Daniel Jackson + */ + +open util/ordering[State] as so +open util/relation as rel + +sig Ref {} +sig Object {} + +-- t->b->v in views when v is view of type t of backing b +-- dirty contains refs that have been invalidated +sig State { + refs: set Ref, + obj: refs -> one Object, + views: ViewType -> refs -> refs, + dirty: set refs +-- , anyviews: Ref -> Ref -- for visualization + } +-- {anyviews = ViewType.views} + +sig Map extends Object { + keys: set Ref, + map: keys -> one Ref + }{all s: State | keys + Ref.map in s.refs} +sig MapRef extends Ref {} +fact {State.obj[MapRef] in Map} + +sig Iterator extends Object { + left, done: set Ref, + lastRef: lone done + }{all s: State | done + left + lastRef in s.refs} +sig IteratorRef extends Ref {} +fact {State.obj[IteratorRef] in Iterator} + +sig Set extends Object { + elts: set Ref + }{all s: State | elts in s.refs} +sig SetRef extends Ref {} +fact {State.obj[SetRef] in Set} + +abstract sig ViewType {} +one sig KeySetView, KeySetView', IteratorView extends ViewType {} +fact ViewTypes { + State.views[KeySetView] in MapRef -> SetRef + State.views[KeySetView'] in SetRef -> MapRef + State.views[IteratorView] in IteratorRef -> SetRef + all s: State | s.views[KeySetView] = ~(s.views[KeySetView']) + } + +/** + * mods is refs modified directly or by view mechanism + * doesn't handle possibility of modifying an object and its view at once? + * should we limit frame conds to non-dirty refs? + */ +pred modifies [pre, post: State, rs: set Ref] { + let vr = pre.views[ViewType], mods = rs.*vr { + all r: pre.refs - mods | pre.obj[r] = post.obj[r] + all b: mods, v: pre.refs, t: ViewType | + b->v in pre.views[t] => viewFrame [t, pre.obj[v], post.obj[v], post.obj[b]] + post.dirty = pre.dirty + + {b: pre.refs | some v: Ref, t: ViewType | + b->v in pre.views[t] && !viewFrame [t, pre.obj[v], post.obj[v], post.obj[b]] + } + } + } + +pred allocates [pre, post: State, rs: set Ref] { + no rs & pre.refs + post.refs = pre.refs + rs + } + +/** + * models frame condition that limits change to view object from v to v' when backing object changes to b' + */ +pred viewFrame [t: ViewType, v, v', b': Object] { + t in KeySetView => v'.elts = dom [b'.map] + t in KeySetView' => b'.elts = dom [v'.map] + t in KeySetView' => (b'.elts) <: (v.map) = (b'.elts) <: (v'.map) + t in IteratorView => v'.elts = b'.left + b'.done + } + +pred MapRef.keySet [pre, post: State, setRefs: SetRef] { + post.obj[setRefs].elts = dom [pre.obj[this].map] + modifies [pre, post, none] + allocates [pre, post, setRefs] + post.views = pre.views + KeySetView->this->setRefs + KeySetView'->setRefs->this + } + +pred MapRef.put [pre, post: State, k, v: Ref] { + post.obj[this].map = pre.obj[this].map ++ k->v + modifies [pre, post, this] + allocates [pre, post, none] + post.views = pre.views + } + +pred SetRef.iterator [pre, post: State, iterRef: IteratorRef] { + let i = post.obj[iterRef] { + i.left = pre.obj[this].elts + no i.done + i.lastRef + } + modifies [pre,post,none] + allocates [pre, post, iterRef] + post.views = pre.views + IteratorView->iterRef->this + } + +pred IteratorRef.remove [pre, post: State] { + let i = pre.obj[this], i' = post.obj[this] { + i'.left = i.left + i'.done = i.done - i.lastRef + no i'.lastRef + } + modifies [pre,post,this] + allocates [pre, post, none] + pre.views = post.views + } + +pred IteratorRef.next [pre, post: State, ref: Ref] { + let i = pre.obj[this], i' = post.obj[this] { + ref in i.left + i'.left = i.left - ref + i'.done = i.done + ref + i'.lastRef = ref + } + modifies [pre, post, this] + allocates [pre, post, none] + pre.views = post.views + } + +pred IteratorRef.hasNext [s: State] { + some s.obj[this].left + } + +assert zippishOK { + all + ks, vs: SetRef, + m: MapRef, + ki, vi: IteratorRef, + k, v: Ref | + let s0=so/first, + s1=so/next[s0], + s2=so/next[s1], + s3=so/next[s2], + s4=so/next[s3], + s5=so/next[s4], + s6=so/next[s5], + s7=so/next[s6] | + ({ + precondition [s0, ks, vs, m] + no s0.dirty + ks.iterator [s0, s1, ki] + vs.iterator [s1, s2, vi] + ki.hasNext [s2] + vi.hasNext [s2] + ki.this/next [s2, s3, k] + vi.this/next [s3, s4, v] + m.put [s4, s5, k, v] + ki.remove [s5, s6] + vi.remove [s6, s7] + } => no State.dirty) + } + +pred precondition [pre: State, ks, vs, m: Ref] { + // all these conditions and other errors discovered in scope of 6 but 8,3 + // in initial state, must have view invariants hold + (all t: ViewType, b, v: pre.refs | + b->v in pre.views[t] => viewFrame [t, pre.obj[v], pre.obj[v], pre.obj[b]]) + // sets are not aliases +-- ks != vs + // sets are not views of map +-- no (ks+vs)->m & ViewType.pre.views + // no iterator currently on either set +-- no Ref->(ks+vs) & ViewType.pre.views + } + +check zippishOK for 6 but 8 State, 3 ViewType expect 1 + +/** + * experiment with controlling heap size + */ +fact {all s: State | #s.obj < 5}