git.iko.soy/Idris-dev
on master help sign in
Added raw (non-typesafe) message passing library

(System.Concurrency.Raw)

commitbba84d503e19ee4298d590c0dd9e5673a978e817 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 30 Oct 2012, 13:29 (14 years ago) parentba6042f
8 files changed+92−7
compare with master
unifiedsplit
lib/System/Concurrency/Raw.idr+25 lib/base.ipkg+4−2 rts/idris_rts.c+8−3 rts/idris_rts.h+4−2 test/README+1 test/test018/expected+15 test/test018/run+4 test/test018/test018.idr+31
lib/System/Concurrency/Raw.idrnew file+25
@@ -0,0 +1,25 @@
1+module System.Concurrency.Raw
2+
3+-- Raw (i.e. not type safe) message passing
4+
5+import System
6+
7+-- Send a message of any type to the thread with the given thread id
8+
9+sendToThread : (thread_id : Ptr) -> a -> IO ()
10+sendToThread {a} dest val
11+ = mkForeign (FFun "idris_sendMessage"
12+ [FPtr, FPtr, FAny a] FUnit) prim__vm dest val
13+
14+checkMsgs : IO Bool
15+checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage"
16+ [FPtr] FInt) prim__vm
17+ return (intToBool msgs)
18+
19+-- Check inbox for messages. If there are none, blocks until a message
20+-- arrives.
21+
22+getMsg : IO a
23+getMsg {a} = mkForeign (FFun "idris_recvMessage"
24+ [FPtr] (FAny a)) prim__vm
25+
lib/base.ipkg+4−2
@@ -5,11 +5,13 @@ modules = Builtins, Prelude, IO, System,
55
66 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8− Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Heap,
9− Prelude.Complex, Prelude.Morphisms,
8+ Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9+ Prelude.Heap, Prelude.Complex, Prelude.Morphisms,
1010
1111 Network.Cgi,
1212
13+ System.Concurrency.Raw,
14+
1315 Language.Reflection,
1416
1517 Control.Monad.Identity, Control.Monad.State, Control.Category,
rts/idris_rts.c+8−3
@@ -424,7 +424,7 @@ VAL copyTo(VM* vm, VAL x) {
424424}
425425
426426// Add a message to another VM's message queue
427−void sendMessage(VM* sender, VM* dest, VAL msg) {
427+void idris_sendMessage(VM* sender, VM* dest, VAL msg) {
428428 // FIXME: If GC kicks in in the middle of the copy, we're in trouble.
429429 // Probably best check there is enough room in advance. (How?)
430430
@@ -457,9 +457,14 @@ void sendMessage(VM* sender, VM* dest, VAL msg) {
457457// printf("Sending [unlock]...\n");
458458}
459459
460+int idris_checkMessages(VM* vm) {
461+ VAL msg = *(vm->inbox_ptr);
462+ return (msg != NULL);
463+}
464+
460465// block until there is a message in the queue
461−VAL recvMessage(VM* vm) {
462− VAL msg = NULL;
466+VAL idris_recvMessage(VM* vm) {
467+ VAL msg;
463468 struct timespec timeout;
464469 int status;
465470
rts/idris_rts.h+4−2
@@ -154,9 +154,11 @@ void* vmThread(VM* callvm, func f, VAL arg);
154154VAL copyTo(VM* newVM, VAL x);
155155
156156// Add a message to another VM's message queue
157−void sendMessage(VM* sender, VM* dest, VAL msg);
157+void idris_sendMessage(VM* sender, VM* dest, VAL msg);
158+// Check whether there are any messages in the queue
159+int idris_checkMessages(VM* vm);
158160// block until there is a message in the queue
159−VAL recvMessage(VM* vm);
161+VAL idris_recvMessage(VM* vm);
160162
161163void dumpVal(VAL r);
162164void dumpStack(VM* vm);
test/README+1
@@ -17,5 +17,6 @@ Tests:
1717015: verified binary adder
1818016: codata
1919017: mutually recursive totality checking
20+018: Message passing concurrency (raw form)
2021
2122regxxx: various regression tests
test/test018/expectednew file+15
@@ -0,0 +1,15 @@
1+Sending
2+Hello!
3+Received
4+Hello to you too!
5+Finished
6+Sending
7+Hello!
8+Received
9+Hello to you too!
10+Finished
11+Sending
12+Hello!
13+Received
14+Hello to you too!
15+Finished
test/test018/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris test018.idr -o test018
3+./test018
4+rm -f test018 *.ibc
test/test018/test018.idrnew file+31
@@ -0,0 +1,31 @@
1+module Main
2+
3+import System
4+import System.Concurrency.Raw
5+
6+recvMsg : IO (Ptr, String)
7+recvMsg = getMsg
8+
9+pong : IO ()
10+pong = do -- putStrLn "Waiting for ping"
11+ (sender, x) <- recvMsg
12+ putStrLn x
13+ putStrLn "Received"
14+ sendToThread sender "Hello to you too!"
15+
16+ping : Ptr -> IO ()
17+ping thread = sendToThread thread (prim__vm, "Hello!")
18+
19+pingpong : IO ()
20+pingpong
21+ = do th <- fork pong
22+ putStrLn "Sending"
23+ ping th
24+ reply <- getMsg
25+ putStrLn reply
26+ usleep 100000
27+ putStrLn "Finished"
28+
29+main : IO ()
30+main = do pingpong; pingpong; pingpong
31+