diff --git a/lib/System/Concurrency/Raw.idr b/lib/System/Concurrency/Raw.idr new file mode 100644 index 000000000..74dbf8b43 --- /dev/null +++ b/lib/System/Concurrency/Raw.idr @@ -0,0 +1,25 @@ +module System.Concurrency.Raw + +-- Raw (i.e. not type safe) message passing + +import System + +-- Send a message of any type to the thread with the given thread id + +sendToThread : (thread_id : Ptr) -> a -> IO () +sendToThread {a} dest val + = mkForeign (FFun "idris_sendMessage" + [FPtr, FPtr, FAny a] FUnit) prim__vm dest val + +checkMsgs : IO Bool +checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage" + [FPtr] FInt) prim__vm + return (intToBool msgs) + +-- Check inbox for messages. If there are none, blocks until a message +-- arrives. + +getMsg : IO a +getMsg {a} = mkForeign (FFun "idris_recvMessage" + [FPtr] (FAny a)) prim__vm + diff --git a/lib/base.ipkg b/lib/base.ipkg index b7fcfea28..82aa83cdb 100644 --- a/lib/base.ipkg +++ b/lib/base.ipkg @@ -5,11 +5,13 @@ modules = Builtins, Prelude, IO, System, Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin, Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative, - Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Heap, - Prelude.Complex, Prelude.Morphisms, + Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, + Prelude.Heap, Prelude.Complex, Prelude.Morphisms, Network.Cgi, + System.Concurrency.Raw, + Language.Reflection, Control.Monad.Identity, Control.Monad.State, Control.Category, diff --git a/rts/idris_rts.c b/rts/idris_rts.c index 3c181ac19..1ab810661 100644 --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -424,7 +424,7 @@ VAL copyTo(VM* vm, VAL x) { } // Add a message to another VM's message queue -void sendMessage(VM* sender, VM* dest, VAL msg) { +void idris_sendMessage(VM* sender, VM* dest, VAL msg) { // FIXME: If GC kicks in in the middle of the copy, we're in trouble. // Probably best check there is enough room in advance. (How?) @@ -457,9 +457,14 @@ void sendMessage(VM* sender, VM* dest, VAL msg) { // printf("Sending [unlock]...\n"); } +int idris_checkMessages(VM* vm) { + VAL msg = *(vm->inbox_ptr); + return (msg != NULL); +} + // block until there is a message in the queue -VAL recvMessage(VM* vm) { - VAL msg = NULL; +VAL idris_recvMessage(VM* vm) { + VAL msg; struct timespec timeout; int status; diff --git a/rts/idris_rts.h b/rts/idris_rts.h index b27cd23fc..6c207089f 100644 --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -154,9 +154,11 @@ void* vmThread(VM* callvm, func f, VAL arg); VAL copyTo(VM* newVM, VAL x); // Add a message to another VM's message queue -void sendMessage(VM* sender, VM* dest, VAL msg); +void idris_sendMessage(VM* sender, VM* dest, VAL msg); +// Check whether there are any messages in the queue +int idris_checkMessages(VM* vm); // block until there is a message in the queue -VAL recvMessage(VM* vm); +VAL idris_recvMessage(VM* vm); void dumpVal(VAL r); void dumpStack(VM* vm); diff --git a/test/README b/test/README index fa7b6653d..603479eb8 100644 --- a/test/README +++ b/test/README @@ -17,5 +17,6 @@ Tests: 015: verified binary adder 016: codata 017: mutually recursive totality checking +018: Message passing concurrency (raw form) regxxx: various regression tests diff --git a/test/test018/expected b/test/test018/expected new file mode 100644 index 000000000..be908ca3a --- /dev/null +++ b/test/test018/expected @@ -0,0 +1,15 @@ +Sending +Hello! +Received +Hello to you too! +Finished +Sending +Hello! +Received +Hello to you too! +Finished +Sending +Hello! +Received +Hello to you too! +Finished diff --git a/test/test018/run b/test/test018/run new file mode 100755 index 000000000..543aae2e8 --- /dev/null +++ b/test/test018/run @@ -0,0 +1,4 @@ +#!/bin/bash +idris test018.idr -o test018 +./test018 +rm -f test018 *.ibc diff --git a/test/test018/test018.idr b/test/test018/test018.idr new file mode 100644 index 000000000..bc0267760 --- /dev/null +++ b/test/test018/test018.idr @@ -0,0 +1,31 @@ +module Main + +import System +import System.Concurrency.Raw + +recvMsg : IO (Ptr, String) +recvMsg = getMsg + +pong : IO () +pong = do -- putStrLn "Waiting for ping" + (sender, x) <- recvMsg + putStrLn x + putStrLn "Received" + sendToThread sender "Hello to you too!" + +ping : Ptr -> IO () +ping thread = sendToThread thread (prim__vm, "Hello!") + +pingpong : IO () +pingpong + = do th <- fork pong + putStrLn "Sending" + ping th + reply <- getMsg + putStrLn reply + usleep 100000 + putStrLn "Finished" + +main : IO () +main = do pingpong; pingpong; pingpong +