bba84d5 · Idris-dev · git.iko.soy

lib/System/Concurrency/Raw.idrnew file+25

compare with master

unifiedsplit

@@ -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,

5

6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8− Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Heap,

8+ Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

9− Prelude.Complex, Prelude.Morphisms,

9+ Prelude.Heap, Prelude.Complex, Prelude.Morphisms,

10

11 Network.Cgi,

12

13+ System.Concurrency.Raw,

14+

13 Language.Reflection,

15 Language.Reflection,

14

16

15 Control.Monad.Identity, Control.Monad.State, Control.Category,

17 Control.Monad.Identity, Control.Monad.State, Control.Category,

rts/idris_rts.c+8−3

@@ -424,7 +424,7 @@ VAL copyTo(VM* vm, VAL x) {

424}

425

426// 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) {

428 // FIXME: If GC kicks in in the middle of the copy, we're in trouble.

429 // Probably best check there is enough room in advance. (How?)

430

@@ -457,9 +457,14 @@ void sendMessage(VM* sender, VM* dest, VAL msg) {

457// printf("Sending [unlock]...\n");

458}

459

460+int idris_checkMessages(VM* vm) {

461+ VAL msg = *(vm->inbox_ptr);

462+ return (msg != NULL);

463+}

464+

460// block until there is a message in the queue

465// block until there is a message in the queue

461−VAL recvMessage(VM* vm) {

466+VAL idris_recvMessage(VM* vm) {

462− VAL msg = NULL;

467+ VAL msg;

463 struct timespec timeout;

468 struct timespec timeout;

464 int status;

469 int status;

465

470

rts/idris_rts.h+4−2

@@ -154,9 +154,11 @@ void* vmThread(VM* callvm, func f, VAL arg);

154VAL copyTo(VM* newVM, VAL x);

155

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

158// block until there is a message in the queue

160// block until there is a message in the queue

159−VAL recvMessage(VM* vm);

161+VAL idris_recvMessage(VM* vm);

160

162

161void dumpVal(VAL r);

163void dumpVal(VAL r);

162void dumpStack(VM* vm);

164void dumpStack(VM* vm);

test/README+1

@@ -17,5 +17,6 @@ Tests:

17015: verified binary adder

18016: codata

19017: mutually recursive totality checking

20+018: Message passing concurrency (raw form)

20

21

21regxxx: various regression tests

22regxxx: 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+