Menu
▾
▴
[Golok-commit] SF.net SVN: golok:[13] trunk
|
From: <sr...@us...> - 2010-03-09 05:10:25
|
Revision: 13
http://golok.svn.sourceforge.net/golok/?rev=13&view=rev
Author: sralmai
Date: 2010-03-09 05:10:18 +0000 (Tue, 09 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: 1e composition is no longer projected. SpinLock is now broken, because with only 1 object, simulation of the fully composed 1e never happens. (But SpinLock-mult works fine.)
Modified Paths:
--------------
trunk/examples/SpinLock.amf
trunk/examples/SpinLock.topo
trunk/examples/dme-mult.amf
trunk/find-k.scm
trunk/golok.scm
trunk/model-builder.scm
trunk/run-all.sh
trunk/search.scm
Added Paths:
-----------
trunk/examples/SpinLock-mult.amf
trunk/examples/SpinLock-mult.topo
trunk/examples/producer-consumer.amf
trunk/examples/producer-consumer.topo
Added: trunk/examples/SpinLock-mult.amf
===================================================================
--- trunk/examples/SpinLock-mult.amf (rev 0)
+++ trunk/examples/SpinLock-mult.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,54 @@
+#
+# SpinLock.amf
+#
+# automata file for Spin Lock
+#
+# David Samuelson
+# August 4, 2009
+#
+
+process thread {
+START: [initial, epsilon ] -> [ Start, begin ]
+REQUEST: [ Start, begin ] -> [Waiting, req ]
+REJECTED: [Waiting, nack ] -> [Waiting, req ]
+ACCEPTED: [Waiting, ack ] -> [Has_Object, in ]
+RELEASING: [Has_Object, in ] -> [Start, rel ]
+
+}
+
+process object {
+REQ_FREE: [NB, req ] -> [ B, ack ]
+REQ_BUSY: [B, req ] -> [ B, nack]
+RCV_REL: [B, rel ] -> [NB, begin]
+
+}
+
+addition-rule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
+}
+
+addition-rule add-object {
+ create: object x
+ foreach thread y {
+ add: var x -- var y
+ }
+}
+
+topology {
+ (object, req, peer)
+ (object, rel, peer)
+ (thread, in, self)
+ (thread, ack, peer)
+ (thread, nack, peer)
+ (thread, begin, peer)
+ (thread, begin, self)
+}
+
+initial-config {
+}
+
+kernel = SpinLock-mult.topo
Added: trunk/examples/SpinLock-mult.topo
===================================================================
--- trunk/examples/SpinLock-mult.topo (rev 0)
+++ trunk/examples/SpinLock-mult.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,12 @@
+model: SpinLock.amf
+
+counts:
+thread 2
+object 2
+
+links:
+
+thread 0 -- object 0
+thread 0 -- object 1
+thread 1 -- object 0
+thread 1 -- object 1
Modified: trunk/examples/SpinLock.amf
===================================================================
--- trunk/examples/SpinLock.amf 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/SpinLock.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -1,11 +1,8 @@
#
# SpinLock.amf
#
-# automata file for Spin Lock
+# behavioral automata for spinlock
#
-# David Samuelson
-# August 4, 2009
-#
process thread {
START: [initial, epsilon ] -> [ Start, begin ]
@@ -23,6 +20,7 @@
}
+
addition-rule add-thread {
create: thread x
foreach object y
@@ -31,13 +29,6 @@
}
}
-addition-rule add-object {
- create: object x
- foreach thread y {
- add: var x -- var y
- }
-}
-
topology {
(object, req, peer)
(object, rel, peer)
@@ -47,7 +38,6 @@
(thread, begin, peer)
(thread, begin, self)
}
-
initial-config {
}
Modified: trunk/examples/SpinLock.topo
===================================================================
--- trunk/examples/SpinLock.topo 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/SpinLock.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -2,11 +2,9 @@
counts:
thread 2
-object 2
+object 1
links:
thread 0 -- object 0
-thread 0 -- object 1
thread 1 -- object 0
-thread 1 -- object 1
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/dme-mult.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -6,12 +6,12 @@
#
#
process forward {
-IDLE: [ Idle, token] -> [ Idle, token]
-SND: [Start, epsilon] -> [Idle, token]
+IDLE: [ Idle, token] -> [ Idle, token2]
+SND: [Start, epsilon] -> [Idle, token2]
}
process critical {
-ENTER: [ Idle, token ] -> [ Cs , in ]
+ENTER: [ Idle, token2 ] -> [ Cs , in ]
LEAVE: [ Cs , in ] -> [ Idle , token ]
}
@@ -31,7 +31,7 @@
}
topology {
- ( critical, token, lpeer)
+ ( critical, token2, lpeer)
( critical, in, self)
( forward, token, lpeer)
}
Added: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf (rev 0)
+++ trunk/examples/producer-consumer.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,81 @@
+process producer {
+
+init: [Init, epsilon] -> [Produced, item]
+produced: [Produced, item] -> [AddBuffer, putprod]
+#recvnak: [WaitMutex, mutexNAKprod] -> [WaitMutex, setprod]
+#recvok: [WaitMutex, mutexOKprod] -> [AddBuffer, putprod]
+addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
+addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
+#recvmutexok: [ClearMutex, mutexCLEARprod] -> [Produced, item]
+}
+
+process consumer {
+init2: [Init2, epsilon] -> [GetBuffer, getcons]
+#recvnak2: [WaitMutex, mutexNAKcons] -> [WaitMutex, setcons]
+#recvok2: [WaitMutex, mutexOKcons] -> [GetBuffer, getcons]
+getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
+getok2: [GetBuffer, bufferOKcons] -> [GetBuffer, getcons]
+#recvreplay: [ClearMutex, mutexCLEARcons] -> [GetBuffer, getcons]
+}
+
+# process mutex {
+# setpassprod: [Clear, setprod] -> [Set, mutexOKprod]
+# setfailprod: [Set, setprod] -> [Set, mutexNAKprod]
+# clearprod: [Set, clearprod] -> [Clear, mutexCLEARprod]
+
+# setpasscons: [Clear, setcons] -> [Set, mutexOKcons]
+# setfailcons: [Set, setcons] -> [Set, mutexNAKcons]
+# clearcons: [Set, clearcons] -> [Clear, mutexCLEARcons]
+# }
+
+
+process buffer {
+ putzeroprod: [Zero, putprod] -> [One, bufferOKprod]
+
+ putoneprod: [One, putprod] -> [One, bufferNAKprod]
+
+ getzerocons: [Zero, getcons] -> [Zero, bufferNAKcons]
+
+ getonecons: [One, getcons] -> [Zero, bufferOKcons]
+
+}
+
+addition-rule add-producer {
+ create: producer x
+# add: var x -- mutex 0
+ add: var x -- buffer 0
+}
+
+addition-rule add-consumer {
+ create: consumer x
+# add: var x -- mutex 0
+ add: var x -- buffer 0
+}
+
+topology {
+ (producer, item, self)
+ (producer, bufferOKprod, peer)
+ (producer, bufferNAKprod, peer)
+# (producer, mutexOKprod, peer)
+# (producer, mutexNAKprod, peer)
+# (producer, mutexCLEARprod, peer)
+ (consumer, bufferOKcons, peer)
+ (consumer, bufferNAKcons, peer)
+# (consumer, mutexOKcons, peer)
+# (consumer, mutexNAKcons, peer)
+# (consumer, mutexCLEARcons, peer)
+
+# (mutex, setprod, peer)
+# (mutex, clearprod, peer)
+ (buffer, putprod, peer)
+
+
+# (mutex, setcons, peer)
+# (mutex, clearcons, peer)
+ (buffer, getcons, peer)
+}
+
+initial-config {
+}
+
+kernel = producer-consumer.topo
Added: trunk/examples/producer-consumer.topo
===================================================================
--- trunk/examples/producer-consumer.topo (rev 0)
+++ trunk/examples/producer-consumer.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,15 @@
+model: producer-consumer.amf
+
+counts:
+
+producer 2
+consumer 2
+buffer 1
+
+links:
+
+producer 0 -- buffer 0
+producer 1 -- buffer 0
+
+consumer 0 -- buffer 0
+consumer 1 -- buffer 0
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/find-k.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -75,6 +75,14 @@
; dump depth
(define dump #f)
+ ; list of non-paramterized process names
+ (define npp (list))
+
+;; TODO: figure out if there is any better way for
+;; passing arguments across modules
+;; (while avoiding circular "requires")
+;; because this is ugly as sin
+;;
;; set globals passed via command line arguments
(define init-clo
(lambda (arg-list)
@@ -90,7 +98,8 @@
(set! stop-depth (list-ref arg-list 8))
(set! process-type (list-ref arg-list 9))
(set! star (list-ref arg-list 10))
- (set! dump (list-ref arg-list 11)))))
+ (set! dump (list-ref arg-list 11))
+ (set! npp (list-ref arg-list 12)))))
;;; internals ;;;
@@ -156,33 +165,34 @@
[starts (if process-type
(let* ([names (protocol-process-names prot)]
[index (item-index process-type names)])
- (if (< index 0) (raise-user-error "Invalid process index ~s" process-type)
+ (cond
+ ((< index 0) (raise-user-error "Invalid process index ~s" process-type))
+ (#t
(begin
(display-ln "INFO: only checking " process-type " for simulation\n")
- (list index))))
+ (list index)))))
; otherwise, check all process indices
(build-list (length (protocol-process-names prot)) values))])
- (for-each
- (lambda (start-aut)
+ ;;
+ ;; TODO: clean this up... should
+ ;;
(for-each
(lambda (x)
(let* ([processes (protocol-process-names prot)]
- [proc-type (list-ref processes x)]
+ [proc-type (automaton-proc-type x)]
[proc-mask (remove proc-type processes)])
(cond
+ ; if this is a non-parameterized process type, skip
+ ((member (automaton-proc-type x) npp) (void))
; if this is an epsilon initiated process and not starting from its start, skip
- ((and (member (list-ref processes x) (map automaton-proc-type eps-auts)) (not (equal? (automaton-proc-type start-aut) (list-ref processes x))))
- (void))
+ ; ((and (member (list-ref processes x) (map automaton-proc-type eps-auts)) (not (equal? (automaton-proc-type start-aut) (list-ref processes x))))
+ ; (void))
(dump-sys
- (model2dot (find-solution x start-aut)
- (string-append output-directory "/" (symbol->string proc-type) "-from-"
- (symbol->string (automaton-proc-type start-aut)) "-sys.dot") proc-mask))
+ (model2dot (find-solution (item-index (automaton-proc-type x) processes) x)
+ (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") proc-mask))
(#t
- (find-solution x start-aut)))))
-
- ; if only checking a single process type, find its index number and return a singleton list
- starts))
+ (find-solution (item-index (automaton-proc-type x) processes) x)))))
eps-auts))
(dump-solution))))
@@ -206,8 +216,7 @@
[mask (remove name names)])
(let-values ([(tt oneE-builder) (build-oneEmodel-builder prot)])
(let ([dummy0 (if dump-1E (model2dot (oneE-builder name start-aut)
- (string-append output-directory "/" (symbol->string name) "-from-"
- (symbol->string (automaton-proc-type start-aut)) "-1e.dot") #:show-buf #f) (void))])
+ (string-append output-directory "/" (symbol->string name) "-1e.dot") #:show-buf #f) (void))])
(let-values ([(soln data) (search prot k name dfs start-aut
#:ring ring
#:dump dump
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/golok.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -8,7 +8,7 @@
(require scheme/cmdline)
;; version header -- should be in form vx.y.z(-tag)
- (define version "v0.1.3.0")
+ (define version "v0.1.4.0")
; parsed values of command line arguments
; currently size 11
@@ -33,9 +33,13 @@
; ring partial order reduction
(define ring #f)
- ; start partial order reduction
+ ; star partial order reduction
(define star (list))
+ ; non-parameterized processes
+ ; TODO: should be able to discover this from addition rules
+ (define npp (list))
+
; just dump the model at a particular depth
(define dump #f)
@@ -50,9 +54,9 @@
; TODO: not implemented
(define stop-depth #f)
- ; index of process type to check
+ ; name of process type to check
(define process-type #f)
-
+
; command line parser which sets up environment
(define amf-file
(command-line
@@ -60,6 +64,7 @@
#:multi
[("--star-point") x "partial order reduction for star" (set! star (cons (string->symbol x) star))]
+ [("--npp" "--non-parameterized-process") x "do not check process type for simulation" (set! npp (cons (string->symbol x) npp))]
#:once-each
[("-t" "--max-time") num "Specify a maximum execution time in seconds before stopping"
@@ -79,8 +84,8 @@
[("--ring") "assume system states are equivalent under rotation" (set! ring #t)]
[("-f" "--start-depth") x "Depth to begin searching for simulation" (set! start-depth (string->number x))]
[("-s" "--stop-depth") x "Depth to halt simulation search" (set! stop-depth (string->number x))]
- [("-p" "--process-type") x "Search only for a specific process" (set! process-type (string->number x))]
+ [("-p" "--process-type") x "Search only for a specific process" (set! process-type (string->symbol x))]
#:args (amf-file) amf-file ))
-(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump))
+(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump npp))
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/model-builder.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -149,7 +149,7 @@
[md (build-model initial-state tt)]
[model (hash->model md tt oneE-flag initial-state)]
;; now filter out the taus and all other transition types
- [stripped (strip-taus model (proc->proc-id proc-type tt) tt)]
+ [stripped (strip-taus-short model (proc->proc-id proc-type tt) tt)]
;; remove all duplicate paths
[cleaned-model (reduce-model stripped)]
;; remove lonely nodes (without transitions to or from)
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/run-all.sh 2010-03-09 05:10:18 UTC (rev 13)
@@ -2,7 +2,7 @@
# this *should* be something nice to ensure stuff works
-TESTS="dme dme-mult SpinLock"
+TESTS="dme dme-mult SpinLock-mult dpp lr-dpp"
make clean
make
@@ -17,12 +17,20 @@
for i in $TESTS
do
echo "Testing BFS"
+ if [[ "$i" == "SpinLock" ]]
+ then
+ ./golok -o output --npp object examples/$i.amf || fail
+ elif [[ "$i" == "producer-consumer" ]]
+ then
+ ./golok -o output --npp buffer examples/$i.amf || fail
+ else
./golok -o output examples/$i.amf || fail
+ fi
make clean
-echo "Testing DFS"
- ./golok -o output --dfs examples/$i.amf || fail
- make clean
+##echo "Testing DFS"
+ # ./golok -o output --dfs examples/$i.amf || fail
+# make clean
done
make clean
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/search.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -137,7 +137,7 @@
(set! state->representative (ring-reducer-init (length (protocol-process-names prot))))))
((not (null? s))
(begin
- (display-ln "INFO: enabling start partial order reduction on " (los->string s))
+ (display-ln "INFO: enabling star partial order reduction on " (los->string s))
(set! state->representative (star-reducer-init ss s lookup-table))))
(#t
(set! state->representative (lambda (x . y) x))))
@@ -378,10 +378,11 @@
(#t
; otherwise, expand all possible branches
; first collect all states reachable via tau transitions
- (let* ([starts (explode state (list proc-type-id))]
+ (let* ([starts (list state)];(explode state (list proc-type-id))]
; then collect all the proc-type transitions possible from the start set
[possibles
- (list-of-lists->list (map (lambda (x) (expand x other-mask-ids #t)) starts))]
+ ;(list-of-lists->list (map (lambda (x) (expand x other-mask-ids #t)) starts))]
+ (list-of-lists->list (map (lambda (x) (expand x (list) #t)) starts))]
; finally sort the transitions according to the needed 1e transitions
[check-list (condense possibles index)])
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
