Menu
▾
▴
[Golok-commit] SF.net SVN: golok:[21] trunk
|
From: <sr...@us...> - 2010-03-24 15:42:14
|
Revision: 21
http://golok.svn.sourceforge.net/golok/?rev=21&view=rev
Author: sralmai
Date: 2010-03-24 15:42:06 +0000 (Wed, 24 Mar 2010)
Log Message:
-----------
[PARSER CHANGE][BROKEN COMMIT]: modified parser to follow the tool paper "topology" section. dme-mult does NOT work (but the part that is most likely the problem will be revamped in the next commit)
Modified Paths:
--------------
trunk/examples/SpinLock-mult.amf
trunk/examples/SpinLock.amf
trunk/examples/dme-mult.amf
trunk/examples/dme.amf
trunk/examples/dpp.amf
trunk/examples/lr-dpp.amf
trunk/examples/milners.amf
trunk/examples/producer-consumer.amf
trunk/find-k.scm
trunk/parser.scm
trunk/run-all.sh
Modified: trunk/examples/SpinLock-mult.amf
===================================================================
--- trunk/examples/SpinLock-mult.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/SpinLock-mult.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,11 +1,8 @@
#
-# SpinLock.amf
+# SpinLock-mult.amf
#
-# automata file for Spin Lock
+# automata file for Spin Lock with multiple locks
#
-# David Samuelson
-# August 4, 2009
-#
process thread {
START: [initial, epsilon ] -> [ Start, begin ]
@@ -23,32 +20,40 @@
}
-addition-rule add-thread {
- create: thread x
- foreach object y
- {
- add: var x -- var y
+
+topology {
+ connectivity {
+ thread 0 -- object 0
+ thread 0 -- object 1
+ thread 1 -- object 0
+ thread 1 -- object 1
}
-}
-addition-rule add-object {
- create: object x
- foreach thread y {
- add: var x -- var y
+ additionrule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
}
-}
+
+ additionrule 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)
+ msgs {
+ (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
Modified: trunk/examples/SpinLock.amf
===================================================================
--- trunk/examples/SpinLock.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/SpinLock.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -20,25 +20,30 @@
}
+topology {
+ connectivity {
+ thread 0 -- object 0
+ thread 1 -- object 0
+ }
-addition-rule add-thread {
- create: thread x
- foreach object y
- {
- add: var x -- var y
+ additionrule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
}
+
+ msgs {
+ (object, req, peer)
+ (object, rel, peer)
+ (thread, in, self)
+ (thread, ack, peer)
+ (thread, nack, peer)
+ (thread, begin, peer)
+ (thread, begin, self)
+ }
}
-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.topo
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dme-mult.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,5 +1,5 @@
#
-# dme-multi.amf
+# dme-mult.amf
#
# implementation of distributed mutual exclusion with
# "normal" nodes and pass nodes (as in "Automating Cut-off..")
@@ -17,27 +17,33 @@
}
# insert two new elements (a pass and a node) into the ring
-addition-rule plain-add {
- require: forward a -> critical 0
- create: critical x
- create: forward y
+topology {
+ connectivity {
+ critical 0 -> forward 0
+ forward 0 -> critical 0
+ }
+
+ additionrule plain-add {
+ create: critical x
+ create: forward y
+
+ require: forward a -> critical 0
- remove: var a -> critical 0
-
- add: var a -> var x
- add: var x -> var y
- add: var y -> critical 0
+ remove: var a -> critical 0
+
+ add: var a -> var x
+ add: var x -> var y
+ add: var y -> critical 0
+ }
+
+ msgs {
+ ( critical, token2, lpeer)
+ ( critical, in, self)
+ ( forward, token, lpeer)
+ }
}
-topology {
- ( critical, token2, lpeer)
- ( critical, in, self)
- ( forward, token, lpeer)
-}
-
initial-config {
( forward 0 SND )
}
-
-kernel = dme-mult.topo
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dme.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -11,22 +11,28 @@
}
-addition-rule plain-add {
- require: node y -> node 0
- create: node x
- remove: var y -> node 0
- add: var y -> var x
- add: var x -> node 0
-}
topology {
- ( node, token, lpeer)
- ( node, in, self)
- ( node, choose, self)
+
+ connectivity {
+ node 0 -> node 0
+ }
+
+ additionrule plain-add {
+ require: node y -> node 0
+ create: node x
+ remove: var y -> node 0
+ add: var y -> var x
+ add: var x -> node 0
+ }
+
+ msgs {
+ ( node, token, lpeer)
+ ( node, in, self)
+ ( node, choose, self)
+ }
}
initial-config {
( node 0 SND )
}
-
-kernel = dme.topo
Modified: trunk/examples/dpp.amf
===================================================================
--- trunk/examples/dpp.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -3,8 +3,6 @@
#
# behavioral automata for dining philosophers protocol
#
-# (for golok v1.2.0)
-#
process diner {
BEGIN: [init, epsilon ] -> [ not-eating, begin ]
@@ -24,41 +22,46 @@
EAT_DONE: [eat, rel_forks] -> [not-eating, begin]
}
-addition-rule add-one {
- create: diner x
- require: diner y -> diner 0
- remove: var y -> diner 0
- add: var y -> var x
- add: var x -> diner 0
-}
topology {
-# (begin, i, i)
-(diner, begin, self)
-
-# (ask_left, i, i - 1)
-(diner, ask_left, rpeer)
-
-# (left_taken, i , i + 1)
-(diner, left_taken, lpeer)
-
-# (left_free, i, i + 1)
-(diner, left_free, lpeer)
-
-# (ask_right, i, i + 1)
-(diner, ask_right, lpeer)
-
-# (right_taken, i , i -1 )
-(diner, right_taken, rpeer)
-
-# (right_free, i, i -1)
-(diner, right_free, rpeer)
-
-# (rel_forks, i, i)
-(diner, rel_forks, self)
+ connectivity {
+ diner 0 -> diner 0
+ }
+
+ additionrule add-one {
+ create: diner x
+ require: diner y -> diner 0
+ remove: var y -> diner 0
+ add: var y -> var x
+ add: var x -> diner 0
+ }
+
+ msgs {
+ # (begin, i, i)
+ (diner, begin, self)
+
+ # (ask_left, i, i - 1)
+ (diner, ask_left, rpeer)
+
+ # (left_taken, i , i + 1)
+ (diner, left_taken, lpeer)
+
+ # (left_free, i, i + 1)
+ (diner, left_free, lpeer)
+
+ # (ask_right, i, i + 1)
+ (diner, ask_right, lpeer)
+
+ # (right_taken, i , i -1 )
+ (diner, right_taken, rpeer)
+
+ # (right_free, i, i -1)
+ (diner, right_free, rpeer)
+
+ # (rel_forks, i, i)
+ (diner, rel_forks, self)
+ }
}
initial-config {
}
-
-kernel = dpp.topo
Modified: trunk/examples/lr-dpp.amf
===================================================================
--- trunk/examples/lr-dpp.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/lr-dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -49,61 +49,69 @@
EAT-DONE2: [eat, rel-forks2] -> [not-eating, begin2]
}
-# add another left and right diner into the ring
-addition-rule add-two {
- create: left-diner x
- create: right-diner y
- require: right-diner z -> left-diner 0
- remove: var z -> left-diner 0
- add: var z -> var x
- add: var x -> var y
- add: var y -> left-diner 0
-}
topology {
-# the general format is:
-#
-# ( process-type, message, link-position )
-#
-
-# (ask-left, i_diner, i-1_diner)
-#
-# this first rule means
-# a left-diner process can receive an
-# ask-left message from is right peer
-#
-# (see lr-dpp.topo for the meaning of
-# right peer)
- (left-diner, ask-left, rpeer)
- (right-diner, ask-left2, rpeer)
-
-# (left-taken, i_diner, i+1_diner)
- (left-diner, left-taken, lpeer)
- (right-diner, left-taken2, lpeer)
-
-# (left-free, i_diner, i+1_diner)
- (left-diner, left-free, lpeer)
- (right-diner, left-free2, lpeer)
-
-# (ask-right, i_diner, i+1_diner)
- (left-diner, ask-right, lpeer)
- (right-diner, ask-right2, lpeer)
-
-# (right-taken, i_diner, i-1_diner)
- (left-diner, right-taken, rpeer)
- (right-diner, right-taken2, rpeer)
-
-# (right-free, i_diner, i-1_diner)
- (left-diner, right-free, rpeer)
- (right-diner, right-free2, rpeer)
-
-# (rel-forks, i_diner, i_diner)
- (left-diner, rel-forks, self)
- (right-diner, rel-forks2, self)
-
-# (self start messages)
- (left-diner, begin, self)
- (right-diner, begin2, self)
+ connectivity {
+ left-diner 0 -> right-diner 0
+ right-diner 0 -> left-diner 0
+ }
+
+ # add another left and right diner into the ring
+ additionrule add-two {
+ create: left-diner x
+ create: right-diner y
+ require: right-diner z -> left-diner 0
+ remove: var z -> left-diner 0
+ add: var z -> var x
+ add: var x -> var y
+ add: var y -> left-diner 0
+ }
+
+ # the general format is:
+ #
+ # ( process-type, message, link-position )
+ #
+
+ # (ask-left, i_diner, i-1_diner)
+ #
+ # this first rule means
+ # a left-diner process can receive an
+ # ask-left message from is right peer
+ #
+ # (see lr-dpp.topo for the meaning of
+ # right peer)
+ msgs {
+ (left-diner, ask-left, rpeer)
+ (right-diner, ask-left2, rpeer)
+
+ # (left-taken, i_diner, i+1_diner)
+ (left-diner, left-taken, lpeer)
+ (right-diner, left-taken2, lpeer)
+
+ # (left-free, i_diner, i+1_diner)
+ (left-diner, left-free, lpeer)
+ (right-diner, left-free2, lpeer)
+
+ # (ask-right, i_diner, i+1_diner)
+ (left-diner, ask-right, lpeer)
+ (right-diner, ask-right2, lpeer)
+
+ # (right-taken, i_diner, i-1_diner)
+ (left-diner, right-taken, rpeer)
+ (right-diner, right-taken2, rpeer)
+
+ # (right-free, i_diner, i-1_diner)
+ (left-diner, right-free, rpeer)
+ (right-diner, right-free2, rpeer)
+
+ # (rel-forks, i_diner, i_diner)
+ (left-diner, rel-forks, self)
+ (right-diner, rel-forks2, self)
+
+ # (self start messages)
+ (left-diner, begin, self)
+ (right-diner, begin2, self)
+ }
}
# no special configuration
@@ -119,5 +127,3 @@
# (init in the automaton RIGHT-START)
initial-config {
}
-
-kernel = lr-dpp.topo
Modified: trunk/examples/milners.amf
===================================================================
--- trunk/examples/milners.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/milners.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -22,23 +22,28 @@
}
-addition-rule plain-add {
- require: scheduler y -> scheduler 0
- create: scheduler x
- remove: var y -> scheduler 0
- add: var y -> var x
- add: var x -> scheduler 0
-}
topology {
- (scheduler,token,lpeer)
- (scheduler,compute,self)
- (scheduler,send-token,self)
+ connectivity {
+ scheduler 0 -> scheduler 1
+ scheduler 1 -> scheduler 0
+ }
+
+ additionrule plain-add {
+ require: scheduler y -> scheduler 0
+ create: scheduler x
+ remove: var y -> scheduler 0
+ add: var y -> var x
+ add: var x -> scheduler 0
+ }
+
+ msgs {
+ (scheduler,token,lpeer)
+ (scheduler,compute,self)
+ (scheduler,send-token,self)
+ }
}
-initial-config{
+initialconfig{
( scheduler 0 INIT )
}
-
-kernel = milners.topo
-
Modified: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/producer-consumer.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,16 +1,16 @@
process producer {
-init: [Init, epsilon] -> [Produced, item]
-produced: [Produced, item] -> [AddBuffer, putprod]
-addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
-addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
+ init: [Init, epsilon] -> [Produced, item]
+ produced: [Produced, item] -> [AddBuffer, putprod]
+ addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
+ addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
}
process consumer {
-init2: [Init2, epsilon] -> [GetBuffer, getcons]
-getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
-getok2: [GetBuffer, bufferOKcons] -> [HasConsumed, in]
-inleave: [HasConsumed, in] -> [GetBuffer, getcons]
+ init2: [Init2, epsilon] -> [GetBuffer, getcons]
+ getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
+ getok2: [GetBuffer, bufferOKcons] -> [HasConsumed, in]
+ inleave: [HasConsumed, in] -> [GetBuffer, getcons]
}
process buffer {
@@ -24,29 +24,38 @@
}
-addition-rule add-producer {
- create: producer x
- add: var x -- buffer 0
-}
-#addition-rule add-consumer {
-# create: consumer x
-# add: var x -- buffer 0
-#}
-
topology {
- (producer, item, self)
- (consumer, in, self)
- (producer, bufferOKprod, peer)
- (producer, bufferNAKprod, peer)
- (consumer, bufferOKcons, peer)
- (consumer, bufferNAKcons, peer)
- (buffer, putprod, peer)
- (buffer, getcons, peer)
+ connectivity {
+ producer 0 -- buffer 0
+ producer 1 -- buffer 0
+ consumer 0 -- buffer 0
+ consumer 1 -- buffer 0
+ }
+
+ additionrule add-producer {
+ create: producer x
+ add: var x -- buffer 0
+ }
+
+ additionrule add-consumer {
+ create: consumer x
+ add: var x -- buffer 0
+ }
+
+ msgs {
+ (producer, item, self)
+ (consumer, in, self)
+ (producer, bufferOKprod, peer)
+ (producer, bufferNAKprod, peer)
+ (consumer, bufferOKcons, peer)
+ (consumer, bufferNAKcons, peer)
+
+ (buffer, putprod, peer)
+ (buffer, getcons, peer)
+ }
}
initial-config {
}
-
-kernel = producer-consumer.topo
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/find-k.scm 2010-03-24 15:42:06 UTC (rev 21)
@@ -139,7 +139,7 @@
(set! start-time (current-seconds))
; k is current system instance
- (set! k (file->topology (string-append amf-directory (protocol-kernel prot))))))))
+ (set! k (protocol-kernel prot))))))
(define parse-filename
(lambda (fn)
Modified: trunk/parser.scm
===================================================================
--- trunk/parser.scm 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/parser.scm 2010-03-24 15:42:06 UTC (rev 21)
@@ -61,15 +61,17 @@
'((whitespace (whitespace) skip)
(comment ("#" (arbno (not #\newline))) skip)
(identifier (letter (arbno (or letter digit "." "_" "/" "-" "?"))) symbol)
- ; (link ("-" (or "-" "E" ">")) symbol)
(number ((or digit "-") (arbno digit)) number)))
(define the-grammar
- '((p_protocol ((arbno "process" p_process) (arbno "addition-rule" addition-rule) p_topology initial-config "kernel" "=" identifier) a-prot)
+ '((p_protocol ((arbno "process" p_process) p_topology initial-config) a-prot)
(p_process (identifier "{" (arbno automaton) "}") a-process)
(automaton (identifier ":" "[" identifier "," identifier "]" "->" "[" identifier "," identifier "]" ) simple-automaton)
+ ;; link is a single entry in the connectivity table
+ (p_link (identifier number link identifier number) a-link)
- (p_topology ( "topology " "{" (arbno p_transition) "}" ) a-p_topology)
+ (p_topology ( "topology " "{" "connectivity" "{" (arbno p_link) "}" (arbno "additionrule" addition-rule) "msgs" "{" (arbno p_transition) "}" "}" ) a-p_topology)
+
(p_transition ("(" identifier "," identifier "," identifier ")") a-p_transition)
(addition-rule (identifier "{" (arbno p_expr) "}") an-addition-rule)
@@ -100,13 +102,23 @@
(link_type link?)
(n2 name?)))
- (define-datatype
- link
- link?
- (peer-link)
- (directed-link)
- (pc-link))
+(define-datatype
+ link
+ link?
+ (peer-link)
+ (directed-link)
+ (pc-link))
+(define-datatype
+ p_link
+ p_link?
+ (a-link
+ (p1 symbol?)
+ (i1 number?)
+ (lt link?)
+ (p2 symbol?)
+ (i2 number?)))
+
(define-datatype
addition-rule
addition-rule?
@@ -158,10 +170,9 @@
p_protocol?
(a-prot
(proc-list (list-of p_process?))
- (add-rule-list (list-of addition-rule?))
(topo p_topology?)
- (init initial-config?)
- (kernel symbol?)))
+ (init initial-config?)))
+
(define-datatype
p_process
@@ -175,8 +186,10 @@
p_topology
p_topology?
(a-p_topology
+ (links (list-of p_link?))
+ (add-rules (list-of addition-rule?))
(trans (list-of p_transition?))))
-
+
(define-datatype
p_transition
p_transition?
@@ -258,29 +271,29 @@
;; read a protocol and return a protocol structure
;;
(define parseProtocol
- (lambda (prot)
+ (lambda (prot filename)
(cases p_protocol prot
- (a-prot (p_processes p_add-rules topo_r init kernel)
- (begin
+ (a-prot (p_processes topo_r init)
+ (cases p_topology topo_r
+ (a-p_topology (p_links p_add-rules p_transitions)
+ (begin
; first do some quick sanity checks
(if (zero? (length p_processes)) (raise-user-error 'PARSE "no processes defined!") (void))
(if (zero? (length p_add-rules)) (raise-user-error 'PARSE "no addition rules defined!") (void))
-
(let* ([procs (map p_proc2proc p_processes)]
[add-rules (map parse-rule p_add-rules)]
- [the-topo (parse-topo topo_r)]
+ [the-topo (parse-topo p_transitions)]
[names (map process-name procs)]
[auts (list-of-lists->list
(map process-auts procs))]
- [start (parse-init init auts)])
- (make-protocol names procs add-rules the-topo start (symbol->string kernel))))))))
+ [start (parse-init init auts)]
+ [kernel (create-kernel filename p_links)])
+ (make-protocol names procs add-rules the-topo start kernel)))))))))
;; topology object -> list of allowed transitions
(define parse-topo
- (lambda (t)
- (cases p_topology t
- (a-p_topology (tr)
- (map trans-unpacker tr)))))
+ (lambda (tr)
+ (map trans-unpacker tr)))
(define trans-unpacker
(lambda (x)
@@ -294,6 +307,11 @@
(the-initial-config (loss)
(map (lambda (x) (parse-start-spec x auts)) loss)))))
+ (define parse_link
+ (lambda (ln)
+ (cases p_link ln
+ (a-link (id1 num1 lt id2 num2) (list id1 num1 (unwrap-lt lt) id2 num2)))))
+
(define parse-start-spec
(lambda (spec auts)
(cases start-spec spec
@@ -309,7 +327,7 @@
(define parse-amf-file
(lambda (x)
- (parseProtocol (s&p_file x))))
+ (parseProtocol (s&p_file x) x)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -488,7 +506,6 @@
(number-name-end (z) (list id z))
(variable-name-end (z) (list id z)))))))
-
; count the number of possible bindings for this requirement
(define count-options
(lambda (x t_links)
@@ -529,3 +546,40 @@
(lambda (x)
(if (eq? sym x) (list proc_t index)
(env x)))))
+
+;;
+;; (string? (list-of link?)) -> topology?
+;;
+(define (create-kernel filename p_links)
+ (let* ([links (map parse_link p_links)]
+ [counts (count-links links)])
+ (make-topology filename counts links)))
+
+;;
+;; (list-of link?
+;;
+(define (count-links links)
+ (let ([db (make-hash)])
+ (begin
+ (count-links-rec links db)
+ (hash-map db (lambda (x y) (list x y))))))
+
+(define (count-links-rec links db)
+ (if (null? links) (void)
+ (let* ([ln (car links)]
+ [name1 (car ln)]
+ [sz1 (second ln)]
+ [name2 (fourth ln)]
+ [sz2 (fifth ln)])
+ (begin
+ (process-link-entry name1 sz1 db)
+ (process-link-entry name2 sz2 db)
+ (count-links-rec (cdr links) db)))))
+
+(define (process-link-entry name sz db)
+ (if (not (hash-has-key? db name))
+ (hash-set! db name (add1 sz))
+ (let ([prev-sz (hash-ref db name)])
+ ;; if already have a larger count, ignore
+ (if (> prev-sz sz) (void)
+ (hash-set! db name (add1 sz))))))
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/run-all.sh 2010-03-24 15:42:06 UTC (rev 21)
@@ -2,7 +2,7 @@
# this *should* be something nice to ensure stuff works
-TESTS="dme dme-mult SpinLock-mult dpp lr-dpp"
+TESTS="dme SpinLock SpinLock-mult dpp lr-dpp"
make clean
make
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
