Added raw (non-typesafe) message passing library

(System.Concurrency.Raw)

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
+

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,

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;
 

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);

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

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

test/test018/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test018.idr -o test018
+./test018
+rm -f test018 *.ibc

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
+