9e58e28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Type safe message passing concurrency

9e58e28Edwin Brady14 years ago

CHANGELOG+1−1

compare with master

unifiedsplit

@@ -9,7 +9,7 @@ User visible changes:

9 elaborating their definitions

10* Implicit arguments will be added automatically only if their initial

11 letter is lower case, or they are in a using declaration

12−* System.Concurrency modules

12+* Added System.Concurrency modules

14New in 0.9.5:

15-------------

lib/System/Concurrency/Process.idrnew file+62

@@ -0,0 +1,62 @@

1+-- WARNING: No guarantees that this works properly yet!

3+module System.Concurrency.Process

5+import System.Concurrency.Raw

7+%access public

9+abstract

10+data ProcID msg = MkPID Ptr

11+

12+-- Type safe message passing programs. Parameterised over the type of

13+-- message which can be send, and the return type.

14+

15+data Process : (msgType : Set) -> Set -> Set where

16+ lift : IO a -> Process msg a

17+

18+instance Monad (Process msg) where

19+ return = lift . return

20+ (lift io) >>= k = lift (do x <- io

21+ case k x of

22+ lift v => v)

23+

24+run : Process msg x -> IO x

25+run (lift prog) = prog

26+

27+-- Get current process ID

28+

29+myID : Process msg (ProcID msg)

30+myID = lift (return (MkPID prim__vm))

31+

32+-- Send a message to another process

33+

34+send : ProcID msg -> msg -> Process msg ()

35+send (MkPID p) m = lift (sendToThread p (prim__vm, m))

36+

37+-- Return whether a message is waiting in the queue

38+

39+msgWaiting : Process msg Bool

40+msgWaiting = lift checkMsgs

41+

42+-- Receive a message - blocks if there is no message waiting

43+

44+recv : Process msg msg

45+recv {msg} = do (senderid, m) <- lift get

46+ return m

47+ where get : IO (Ptr, msg)

48+ get = getMsg

49+

50+-- receive a message, and return with the sender's process ID.

51+

52+recvWithSender : Process msg (ProcID msg, msg)

53+recvWithSender {msg}

54+ = do (senderid, m) <- lift get

55+ return (MkPID senderid, m)

56+ where get : IO (Ptr, msg)

57+ get = getMsg

58+

59+create : |(thread : Process msg ()) -> Process msg (ProcID msg)

60+create (lift p) = do ptr <- lift (fork p)

61+ return (MkPID ptr)

62+

lib/System/Concurrency/Raw.idr+2

@@ -1,3 +1,5 @@

1+-- WARNING: No guarantees that this works properly yet!

1module System.Concurrency.Raw

3module System.Concurrency.Raw

3-- Raw (i.e. not type safe) message passing

5-- Raw (i.e. not type safe) message passing

lib/base.ipkg+1−1

@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO, System,

11 Network.Cgi,

13− System.Concurrency.Raw,

13+ System.Concurrency.Raw, System.Concurrency.Process,

15 Language.Reflection,

rts/idris_gc.c+9−9

@@ -11,7 +11,7 @@ VAL copy(VM* vm, VAL x) {

11 }

12 switch(GETTY(x)) {

13 case CON:

14− cl = allocCon(vm, x->info.c.arity);

14+ cl = allocCon(vm, x->info.c.arity, 1);

15 cl->info.c.tag = x->info.c.tag;

16 cl->info.c.arity = x->info.c.arity;

@@ -23,16 +23,16 @@ VAL copy(VM* vm, VAL x) {

23 }

24 break;

25 case FLOAT:

26− cl = MKFLOAT(vm, x->info.f);

26+ cl = MKFLOATc(vm, x->info.f);

27 break;

28 case STRING:

29− cl = MKSTR(vm, x->info.str);

29+ cl = MKSTRc(vm, x->info.str);

30 break;

31 case BIGINT:

32− cl = MKBIGM(vm, x->info.ptr);

32+ cl = MKBIGMc(vm, x->info.ptr);

33 break;

34 case PTR:

35− cl = MKPTR(vm, x->info.ptr);

35+ cl = MKPTRc(vm, x->info.ptr);

36 break;

37 case FWD:

38 return x->info.ptr;

@@ -72,7 +72,7 @@ void cheney(VM *vm) {

72 assert(scan == vm->heap_next);

73}

75−void gc(VM* vm) {

75+void idris_gc(VM* vm) {

76 // printf("Collecting\n");

78 char* newheap = malloc(vm -> heap_size);

@@ -108,16 +108,16 @@ void gc(VM* vm) {

108 vm->heap_size += vm->heap_growth;

109 }

110 vm->oldheap = oldheap;

111−

111+

112 // gcInfo(vm, 0);

113}

114

115−void gcInfo(VM* vm, int doGC) {

115+void idris_gcInfo(VM* vm, int doGC) {

116 printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

117 printf("Total allocations: %d\n", vm->allocations);

118 printf("GCs: %d\n", vm->collections);

119 printf("Final heap size %d\n", (int)(vm->heap_size));

120 printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));

121− if (doGC) { gc(vm); }

121+ if (doGC) { idris_gc(vm); }

122 printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));

123}

rts/idris_gc.h+2−2

@@ -3,7 +3,7 @@

4#include "idris_rts.h"

6−void gc(VM* vm);

6+void idris_gc(VM* vm);

7−void gcInfo(VM* vm, int doGC);

7+void idris_gcInfo(VM* vm, int doGC);

9#endif

rts/idris_gmp.c+30−14

@@ -9,8 +9,9 @@ VAL MKBIGI(int val) {

10VAL MKBIGC(VM* vm, char* val) {

11 mpz_t* bigint;

12+ // FIXME! what if GC happens after cl allocation?

12− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

13+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

13− bigint = allocate(vm, sizeof(mpz_t));

14+ bigint = allocate(vm, sizeof(mpz_t), 0);

15 mpz_init(*bigint);

16 mpz_init(*bigint);

16 mpz_set_str(*bigint, val, 10);

17 mpz_set_str(*bigint, val, 10);

@@ -23,8 +24,23 @@ VAL MKBIGC(VM* vm, char* val) {

24VAL MKBIGM(VM* vm, void* big) {

25VAL MKBIGM(VM* vm, void* big) {

25 mpz_t* bigint;

26 mpz_t* bigint;

27+ // FIXME! what if GC happens after cl allocation?

28+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

29+ bigint = allocate(vm, sizeof(mpz_t), 0);

30+

31+ mpz_init(*bigint);

32+ mpz_set(*bigint, *((mpz_t*)big));

33+

34+ SETTY(cl, BIGINT);

35+ cl -> info.ptr = (void*)bigint;

36+

37+ return cl;

38+}

39+

40+VAL MKBIGMc(VM* vm, void* big) {

41+ mpz_t* bigint;

26− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

42+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 1);

27− bigint = allocate(vm, sizeof(mpz_t));

43+ bigint = allocate(vm, sizeof(mpz_t), 1);

29 mpz_init(*bigint);

45 mpz_init(*bigint);

30 mpz_set(*bigint, *((mpz_t*)big));

46 mpz_set(*bigint, *((mpz_t*)big));

@@ -38,8 +54,8 @@ VAL MKBIGM(VM* vm, void* big) {

38VAL GETBIG(VM * vm, VAL x) {

54VAL GETBIG(VM * vm, VAL x) {

39 if (ISINT(x)) {

55 if (ISINT(x)) {

40 mpz_t* bigint;

56 mpz_t* bigint;

41− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

57+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

42− bigint = allocate(vm, sizeof(mpz_t));

58+ bigint = allocate(vm, sizeof(mpz_t), 0);

44 mpz_init(*bigint);

60 mpz_init(*bigint);

45 mpz_set_si(*bigint, GETINT(x));

61 mpz_set_si(*bigint, GETINT(x));

@@ -55,8 +71,8 @@ VAL GETBIG(VM * vm, VAL x) {

56VAL bigAdd(VM* vm, VAL x, VAL y) {

72VAL bigAdd(VM* vm, VAL x, VAL y) {

57 mpz_t* bigint;

73 mpz_t* bigint;

58− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

74+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

59− bigint = allocate(vm, sizeof(mpz_t));

75+ bigint = allocate(vm, sizeof(mpz_t), 0);

60 mpz_add(*bigint, GETMPZ(x), GETMPZ(y));

76 mpz_add(*bigint, GETMPZ(x), GETMPZ(y));

61 SETTY(cl, BIGINT);

77 SETTY(cl, BIGINT);

62 cl -> info.ptr = (void*)bigint;

78 cl -> info.ptr = (void*)bigint;

@@ -65,8 +81,8 @@ VAL bigAdd(VM* vm, VAL x, VAL y) {

66VAL bigSub(VM* vm, VAL x, VAL y) {

82VAL bigSub(VM* vm, VAL x, VAL y) {

67 mpz_t* bigint;

83 mpz_t* bigint;

68− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

84+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

69− bigint = allocate(vm, sizeof(mpz_t));

85+ bigint = allocate(vm, sizeof(mpz_t), 0);

70 mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));

86 mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));

71 SETTY(cl, BIGINT);

87 SETTY(cl, BIGINT);

72 cl -> info.ptr = (void*)bigint;

88 cl -> info.ptr = (void*)bigint;

@@ -75,8 +91,8 @@ VAL bigSub(VM* vm, VAL x, VAL y) {

76VAL bigMul(VM* vm, VAL x, VAL y) {

92VAL bigMul(VM* vm, VAL x, VAL y) {

77 mpz_t* bigint;

93 mpz_t* bigint;

78− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

94+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

79− bigint = allocate(vm, sizeof(mpz_t));

95+ bigint = allocate(vm, sizeof(mpz_t), 0);

80 mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));

96 mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));

81 SETTY(cl, BIGINT);

97 SETTY(cl, BIGINT);

82 cl -> info.ptr = (void*)bigint;

98 cl -> info.ptr = (void*)bigint;

@@ -85,8 +101,8 @@ VAL bigMul(VM* vm, VAL x, VAL y) {

101

86VAL bigDiv(VM* vm, VAL x, VAL y) {

102VAL bigDiv(VM* vm, VAL x, VAL y) {

87 mpz_t* bigint;

103 mpz_t* bigint;

88− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

104+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

89− bigint = allocate(vm, sizeof(mpz_t));

105+ bigint = allocate(vm, sizeof(mpz_t), 0);

90 mpz_div(*bigint, GETMPZ(x), GETMPZ(y));

106 mpz_div(*bigint, GETMPZ(x), GETMPZ(y));

91 SETTY(cl, BIGINT);

107 SETTY(cl, BIGINT);

92 cl -> info.ptr = (void*)bigint;

108 cl -> info.ptr = (void*)bigint;

rts/idris_gmp.h+1

@@ -4,6 +4,7 @@

4VAL MKBIGI(int val);

5VAL MKBIGC(VM* vm, char* bigint);

6VAL MKBIGM(VM* vm, void* bigint);

7+VAL MKBIGMc(VM* vm, void* bigint);

8VAL idris_bigPlus(VM*, VAL x, VAL y);

9VAL idris_bigPlus(VM*, VAL x, VAL y);

9VAL idris_bigMinus(VM*, VAL x, VAL y);

10VAL idris_bigMinus(VM*, VAL x, VAL y);

rts/idris_main.c+1−1

@@ -3,7 +3,7 @@ int main(int argc, char* argv[]) {

3 _idris__123_runMain0_125_(vm, NULL);

4 //_idris_main(vm, NULL);

5#ifdef IDRIS_TRACE

6− gcInfo(vm, 1);

6+ idris_gcInfo(vm, 1);

7#endif

8 terminate(vm);

rts/idris_rts.c+86−23

@@ -37,15 +37,18 @@ VM* init_vm(int stack_size, size_t heap_size,

37 vm->reg1 = NULL;

39 vm->inbox = malloc(1024*sizeof(VAL));

40+ memset(vm->inbox, 0, 1024*sizeof(VAL));

40 vm->inbox_end = vm->inbox + 1024;

41 vm->inbox_end = vm->inbox + 1024;

41 vm->inbox_ptr = vm->inbox;

42 vm->inbox_ptr = vm->inbox;

42 vm->inbox_write = vm->inbox;

43 vm->inbox_write = vm->inbox;

44 pthread_mutex_init(&(vm->inbox_lock), NULL);

45 pthread_mutex_init(&(vm->inbox_lock), NULL);

45 pthread_mutex_init(&(vm->inbox_block), NULL);

46 pthread_mutex_init(&(vm->inbox_block), NULL);

47+ pthread_mutex_init(&(vm->alloc_lock), NULL);

46 pthread_cond_init(&(vm->inbox_waiting), NULL);

48 pthread_cond_init(&(vm->inbox_waiting), NULL);

48 vm->max_threads = max_threads;

50 vm->max_threads = max_threads;

51+ vm->processes = 0;

50 int i;

53 int i;

51 // Assumption: there's enough space for this in the initial heap.

54 // Assumption: there's enough space for this in the initial heap.

@@ -73,8 +76,14 @@ void terminate(VM* vm) {

73 free(vm);

76 free(vm);

74}

77}

76−void* allocate(VM* vm, size_t size) {

79+void* allocate(VM* vm, size_t size, int outerlock) {

77// return malloc(size);

80// return malloc(size);

81+ int lock = vm->processes > 0 && !outerlock;

82+

83+ if (lock) { // not message passing

84+ pthread_mutex_lock(&vm->alloc_lock);

85+ }

86+

78 if ((size & 7)!=0) {

87 if ((size & 7)!=0) {

79 size = 8 + ((size >> 3) << 3);

88 size = 8 + ((size >> 3) << 3);

80 }

89 }

@@ -84,15 +93,23 @@ void* allocate(VM* vm, size_t size) {

84 *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

93 *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

85 vm -> heap_next += size + sizeof(size_t);

94 vm -> heap_next += size + sizeof(size_t);

86 memset(ptr, 0, size);

95 memset(ptr, 0, size);

96+ if (lock) { // not message passing

97+ pthread_mutex_unlock(&vm->alloc_lock);

98+ }

87 return ptr;

99 return ptr;

88 } else {

100 } else {

89− gc(vm);

101+ idris_gc(vm);

102+ if (lock) { // not message passing

103+ pthread_mutex_unlock(&vm->alloc_lock);

104+ }

90− return allocate(vm, size);

105+ return allocate(vm, size, 0);

91 }

106 }

107+

92}

108}

109

94−void* allocCon(VM* vm, int arity) {

110+void* allocCon(VM* vm, int arity, int outer) {

95− Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity);

111+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity,

112+ outer);

96 SETTY(cl, CON);

113 SETTY(cl, CON);

97 if (arity == 0) {

114 if (arity == 0) {

98 cl -> info.c.args = NULL;

115 cl -> info.c.args = NULL;

@@ -106,7 +123,7 @@ void* allocCon(VM* vm, int arity) {

106}

123}

107

124

108VAL MKFLOAT(VM* vm, double val) {

125VAL MKFLOAT(VM* vm, double val) {

109− Closure* cl = allocate(vm, sizeof(Closure));

126+ Closure* cl = allocate(vm, sizeof(Closure), 0);

110 SETTY(cl, FLOAT);

127 SETTY(cl, FLOAT);

111 cl -> info.f = val;

128 cl -> info.f = val;

112 return cl;

129 return cl;

@@ -114,7 +131,7 @@ VAL MKFLOAT(VM* vm, double val) {

114

131

115VAL MKSTR(VM* vm, char* str) {

132VAL MKSTR(VM* vm, char* str) {

116 Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +

133 Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +

117− sizeof(char)*strlen(str)+1);

134+ sizeof(char)*strlen(str)+1, 0);

118 SETTY(cl, STRING);

135 SETTY(cl, STRING);

119 cl -> info.str = (char*)cl + sizeof(Closure);

136 cl -> info.str = (char*)cl + sizeof(Closure);

120

137

@@ -123,7 +140,31 @@ VAL MKSTR(VM* vm, char* str) {

123}

140}

124

141

125VAL MKPTR(VM* vm, void* ptr) {

142VAL MKPTR(VM* vm, void* ptr) {

126− Closure* cl = allocate(vm, sizeof(Closure));

143+ Closure* cl = allocate(vm, sizeof(Closure), 0);

144+ SETTY(cl, PTR);

145+ cl -> info.ptr = ptr;

146+ return cl;

147+}

148+

149+VAL MKFLOATc(VM* vm, double val) {

150+ Closure* cl = allocate(vm, sizeof(Closure), 1);

151+ SETTY(cl, FLOAT);

152+ cl -> info.f = val;

153+ return cl;

154+}

155+

156+VAL MKSTRc(VM* vm, char* str) {

157+ Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +

158+ sizeof(char)*strlen(str)+1, 1);

159+ SETTY(cl, STRING);

160+ cl -> info.str = (char*)cl + sizeof(Closure);

161+

162+ strcpy(cl -> info.str, str);

163+ return cl;

164+}

165+

166+VAL MKPTRc(VM* vm, void* ptr) {

167+ Closure* cl = allocate(vm, sizeof(Closure), 1);

127 SETTY(cl, PTR);

168 SETTY(cl, PTR);

128 cl -> info.ptr = ptr;

169 cl -> info.ptr = ptr;

129 return cl;

170 return cl;

@@ -211,7 +252,7 @@ void dumpVal(VAL v) {

211}

252}

212

253

213VAL idris_castIntStr(VM* vm, VAL i) {

254VAL idris_castIntStr(VM* vm, VAL i) {

214− Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16);

255+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

215 SETTY(cl, STRING);

256 SETTY(cl, STRING);

216 cl -> info.str = (char*)cl + sizeof(Closure);

257 cl -> info.str = (char*)cl + sizeof(Closure);

217 sprintf(cl -> info.str, "%d", (int)(GETINT(i)));

258 sprintf(cl -> info.str, "%d", (int)(GETINT(i)));

@@ -228,7 +269,7 @@ VAL idris_castStrInt(VM* vm, VAL i) {

228}

269}

229

270

230VAL idris_castFloatStr(VM* vm, VAL i) {

271VAL idris_castFloatStr(VM* vm, VAL i) {

231− Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32);

272+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32, 0);

232 SETTY(cl, STRING);

273 SETTY(cl, STRING);

233 cl -> info.str = (char*)cl + sizeof(Closure);

274 cl -> info.str = (char*)cl + sizeof(Closure);

234 sprintf(cl -> info.str, "%g", GETFLOAT(i));

275 sprintf(cl -> info.str, "%g", GETFLOAT(i));

@@ -244,7 +285,8 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {

244 char *ls = GETSTR(l);

285 char *ls = GETSTR(l);

245 // dumpVal(l);

286 // dumpVal(l);

246 // printf("\n");

287 // printf("\n");

247− Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1);

288+ Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1,

289+ 0);

248 SETTY(cl, STRING);

290 SETTY(cl, STRING);

249 cl -> info.str = (char*)cl + sizeof(Closure);

291 cl -> info.str = (char*)cl + sizeof(Closure);

250 strcpy(cl -> info.str, ls);

292 strcpy(cl -> info.str, ls);

@@ -319,7 +361,7 @@ VAL idris_strTail(VM* vm, VAL str) {

319VAL idris_strCons(VM* vm, VAL x, VAL xs) {

361VAL idris_strCons(VM* vm, VAL x, VAL xs) {

320 char *xstr = GETSTR(xs);

362 char *xstr = GETSTR(xs);

321 Closure* cl = allocate(vm, sizeof(Closure) +

363 Closure* cl = allocate(vm, sizeof(Closure) +

322− strlen(xstr) + 2);

364+ strlen(xstr) + 2, 0);

323 SETTY(cl, STRING);

365 SETTY(cl, STRING);

324 cl -> info.str = (char*)cl + sizeof(Closure);

366 cl -> info.str = (char*)cl + sizeof(Closure);

325 cl -> info.str[0] = (char)(GETINT(x));

367 cl -> info.str[0] = (char)(GETINT(x));

@@ -334,7 +376,7 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i) {

334VAL idris_strRev(VM* vm, VAL str) {

376VAL idris_strRev(VM* vm, VAL str) {

335 char *xstr = GETSTR(str);

377 char *xstr = GETSTR(str);

336 Closure* cl = allocate(vm, sizeof(Closure) +

378 Closure* cl = allocate(vm, sizeof(Closure) +

337− strlen(xstr) + 1);

379+ strlen(xstr) + 1, 0);

338 SETTY(cl, STRING);

380 SETTY(cl, STRING);

339 cl -> info.str = (char*)cl + sizeof(Closure);

381 cl -> info.str = (char*)cl + sizeof(Closure);

340 int y = 0;

382 int y = 0;

@@ -348,7 +390,8 @@ VAL idris_strRev(VM* vm, VAL str) {

348}

390}

349

391

350typedef struct {

392typedef struct {

351− VM* vm;

393+ VM* vm; // thread's VM

394+ VM* callvm; // calling thread's VM

352 func fn;

395 func fn;

353 VAL arg;

396 VAL arg;

354} ThreadData;

397} ThreadData;

@@ -356,13 +399,16 @@ typedef struct {

356void* runThread(void* arg) {

399void* runThread(void* arg) {

357 ThreadData* td = (ThreadData*)arg;

400 ThreadData* td = (ThreadData*)arg;

358 VM* vm = td->vm;

401 VM* vm = td->vm;

402+ VM* callvm = td->callvm;

359

403

360 TOP(0) = td->arg;

404 TOP(0) = td->arg;

361 BASETOP(0);

405 BASETOP(0);

362 ADDTOP(1);

406 ADDTOP(1);

363 td->fn(vm, NULL);

407 td->fn(vm, NULL);

408+ callvm->processes--;

364

409

365 free(td);

410 free(td);

411+ terminate(vm);

366 return NULL;

412 return NULL;

367}

413}

368

414

@@ -370,6 +416,7 @@ void* vmThread(VM* callvm, func f, VAL arg) {

370 VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size,

416 VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size,

371 callvm->max_threads,

417 callvm->max_threads,

372 0, NULL);

418 0, NULL);

419+ vm->processes=1; // since it can send and receive messages

373 pthread_t t;

420 pthread_t t;

374 pthread_attr_t attr;

421 pthread_attr_t attr;

375// size_t stacksize;

422// size_t stacksize;

@@ -380,16 +427,18 @@ void* vmThread(VM* callvm, func f, VAL arg) {

380

427

381 ThreadData *td = malloc(sizeof(ThreadData));

428 ThreadData *td = malloc(sizeof(ThreadData));

382 td->vm = vm;

429 td->vm = vm;

430+ td->callvm = callvm;

383 td->fn = f;

431 td->fn = f;

384 td->arg = copyTo(vm, arg);

432 td->arg = copyTo(vm, arg);

433+

434+ callvm->processes++;

385

435

386 pthread_create(&t, &attr, runThread, td);

436 pthread_create(&t, &attr, runThread, td);

387// usleep(100);

437// usleep(100);

388 return vm;

438 return vm;

389}

439}

390

440

391−// VM is assumed to be a different vm from the one x lives on (so we don't need

441+// VM is assumed to be a different vm from the one x lives on

392−// to worry about gc moving things, as the VM x is on will not be allocating)

393

442

394VAL copyTo(VM* vm, VAL x) {

443VAL copyTo(VM* vm, VAL x) {

395 int i;

444 int i;

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

400 }

449 }

401 switch(GETTY(x)) {

450 switch(GETTY(x)) {

402 case CON:

451 case CON:

403− cl = allocCon(vm, x->info.c.arity);

452+ cl = allocCon(vm, x->info.c.arity, 1);

404 cl->info.c.tag = x->info.c.tag;

453 cl->info.c.tag = x->info.c.tag;

405 cl->info.c.arity = x->info.c.arity;

454 cl->info.c.arity = x->info.c.arity;

406

455

@@ -411,16 +460,16 @@ VAL copyTo(VM* vm, VAL x) {

411 }

460 }

412 break;

461 break;

413 case FLOAT:

462 case FLOAT:

414− cl = MKFLOAT(vm, x->info.f);

463+ cl = MKFLOATc(vm, x->info.f);

415 break;

464 break;

416 case STRING:

465 case STRING:

417− cl = MKSTR(vm, x->info.str);

466+ cl = MKSTRc(vm, x->info.str);

418 break;

467 break;

419 case BIGINT:

468 case BIGINT:

420− cl = MKBIGM(vm, x->info.ptr);

469+ cl = MKBIGMc(vm, x->info.ptr);

421 break;

470 break;

422 case PTR:

471 case PTR:

423− cl = MKPTR(vm, x->info.ptr);

472+ cl = MKPTRc(vm, x->info.ptr);

424 break;

473 break;

425 default:

474 default:

426 assert(0); // We're in trouble if this happens...

475 assert(0); // We're in trouble if this happens...

@@ -433,12 +482,26 @@ void idris_sendMessage(VM* sender, VM* dest, VAL msg) {

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

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

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

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

435

484

485+ // Also a problem if we're allocating at the same time as the

486+ // destination thread (which is very likely)

487+ // Should the inbox be a different memory space?

488+

489+ // So: we try to copy, if a collection happens, we do the copy again

490+ // under the assumption there's enough space this time.

491+

492+ int gcs = dest->collections;

493+ pthread_mutex_lock(&dest->alloc_lock);

436 VAL dmsg = copyTo(dest, msg);

494 VAL dmsg = copyTo(dest, msg);

495+ pthread_mutex_unlock(&dest->alloc_lock);

437

496

497+ if (dest->collections>gcs) {

498+ // a collection will have invalidated the copy

499+ pthread_mutex_lock(&dest->alloc_lock);

500+ dmsg = copyTo(dest, msg); // try again now there's room...

501+ pthread_mutex_unlock(&dest->alloc_lock);

502+ }

438

503

439−// printf("Sending [lock]...\n");

440 pthread_mutex_lock(&(dest->inbox_lock));

504 pthread_mutex_lock(&(dest->inbox_lock));

441−

442 *(dest->inbox_write) = dmsg;

505 *(dest->inbox_write) = dmsg;

443

506

444 dest->inbox_write++;

507 dest->inbox_write++;

rts/idris_rts.h+9−2

@@ -51,6 +51,7 @@ typedef struct {

52 pthread_mutex_t inbox_lock;

53 pthread_mutex_t inbox_block;

54+ pthread_mutex_t alloc_lock;

54 pthread_cond_t inbox_waiting;

55 pthread_cond_t inbox_waiting;

56 VAL* inbox; // Block of memory for storing messages

57 VAL* inbox; // Block of memory for storing messages

@@ -59,6 +60,7 @@ typedef struct {

59 VAL* inbox_ptr; // Next message to read

60 VAL* inbox_ptr; // Next message to read

60 VAL* inbox_write; // Location of next message to write

61 VAL* inbox_write; // Location of next message to write

63+ int processes; // Number of child processes

62 int max_threads; // maximum number of threads to run in parallel

64 int max_threads; // maximum number of threads to run in parallel

64 int argc;

66 int argc;

@@ -140,6 +142,11 @@ VAL MKFLOAT(VM* vm, double val);

140VAL MKSTR(VM* vm, char* str);

142VAL MKSTR(VM* vm, char* str);

141VAL MKPTR(VM* vm, void* ptr);

143VAL MKPTR(VM* vm, void* ptr);

142

144

145+// following versions don't take a lock when allocating

146+VAL MKFLOATc(VM* vm, double val);

147+VAL MKSTRc(VM* vm, char* str);

148+VAL MKPTRc(VM* vm, void* ptr);

149+

143VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);

150VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);

144

151

145#define SETTAG(x, a) (x)->info.c.tag = (a)

152#define SETTAG(x, a) (x)->info.c.tag = (a)

@@ -149,8 +156,8 @@ VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);

149void PROJECT(VM* vm, VAL r, int loc, int arity);

156void PROJECT(VM* vm, VAL r, int loc, int arity);

150void SLIDE(VM* vm, int args);

157void SLIDE(VM* vm, int args);

151

158

152−void* allocate(VM* vm, size_t size);

159+void* allocate(VM* vm, size_t size, int outerlock);

153−void* allocCon(VM* vm, int arity);

160+void* allocCon(VM* vm, int arity, int outerlock);

154

161

155void* vmThread(VM* callvm, func f, VAL arg);

162void* vmThread(VM* callvm, func f, VAL arg);

156

163

src/Core/CaseTree.hs+8−8

@@ -58,18 +58,18 @@ type Clause = ([Pat], (Term, Term))

58type CS = ([Term], Int)

60instance TermSize SC where

61− termsize (Case n as) = termsize as

61+ termsize n (Case n' as) = termsize n as

62− termsize (STerm t) = termsize t

62+ termsize n (STerm t) = termsize n t

63− termsize _ = 1

63+ termsize n _ = 1

65instance TermSize CaseAlt where

66− termsize (ConCase _ _ _ s) = termsize s

66+ termsize n (ConCase _ _ _ s) = termsize n s

67− termsize (ConstCase _ s) = termsize s

67+ termsize n (ConstCase _ s) = termsize n s

68− termsize (DefaultCase s) = termsize s

68+ termsize n (DefaultCase s) = termsize n s

70-- simple terms can be inlined trivially - good for primitives in particular

71−small :: SC -> Bool

71+small :: Name -> SC -> Bool

72−small t = False -- termsize t < 150

72+small n t = False -- termsize n t < 10

74namesUsed :: SC -> [Name]

75namesUsed sc = nub $ nu' [] sc where

src/Core/Evaluate.hs+1−1

@@ -707,7 +707,7 @@ addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt

707 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

708 simpleCase tcase covering RunTime (FC "" 0) psrt) of

709 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

710− let inl = alwaysInline || small sc' in

710+ let inl = alwaysInline || small n sc' in

711 addDef n (CaseOp inl ty ps_in ps args sc args' sc',

712 access, Unchecked) ctxt in

713 uctxt { definitions = ctxt' }

src/Core/TT.hs+14−10

@@ -434,18 +434,22 @@ deriving instance Binary TT

434!-}

435

436class TermSize a where

437− termsize :: a -> Int

437+ termsize :: Name -> a -> Int

438

439instance TermSize a => TermSize [a] where

440− termsize [] = 0

440+ termsize n [] = 0

441− termsize (x : xs) = termsize x + termsize xs

441+ termsize n (x : xs) = termsize n x + termsize n xs

442−

442+

443−instance TermSize (TT a) where

443+instance TermSize (TT Name) where

444− termsize (P _ _ _) = 1

444+ termsize n (P _ x _)

445+ | x == n = 1000000 -- recursive => really big

446+ | otherwise = 1

445− termsize (V _) = 1

447+ termsize n (V _) = 1

446− termsize (Bind n (Let t v) sc) = termsize v + termsize sc

448+ termsize n (Bind n' (Let t v) sc)

449+ = let rn = if n == n' then MN 0 "noname" else n in

450+ termsize rn v + termsize rn sc

447− termsize (App f a) = termsize f + termsize a

451+ termsize n (App f a) = termsize n f + termsize n a

448− termsize _ = 1

452+ termsize n _ = 1

449

453

450instance Sized a => Sized (TT a) where

454instance Sized a => Sized (TT a) where

451 size (P name n trm) = 1 + size name + size n + size trm

455 size (P name n trm) = 1 + size name + size n + size trm

src/IRTS/CodegenC.hs+1−1

@@ -100,7 +100,7 @@ bcc i (ASSIGNCONST l c)

100 mkConst _ = "MKINT(42424242)"

101bcc i (MKCON l tag args)

102 = indent i ++ creg Tmp ++ " = allocCon(vm, " ++ show (length args) ++

103− "); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" ++

103+ ", 0); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" ++

104 indent i ++ setArgs 0 args ++ "\n" ++

105 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

106

test/test018/expected+500

@@ -13,3 +13,503 @@ Hello!

13Received

14Hello to you too!

15Finished

16+100

17+Waiting for message

18+Sent ping

19+Received Hello!

20+Reply: Hello back!

21+99

22+Waiting for message

23+Sent ping

24+Received Hello!

25+Reply: Hello back!

26+98

27+Waiting for message

28+Sent ping

29+Received Hello!

30+Reply: Hello back!

31+97

32+Waiting for message

33+Sent ping

34+Received Hello!

35+Reply: Hello back!

36+96

37+Waiting for message

38+Sent ping

39+Received Hello!

40+Reply: Hello back!

41+95

42+Waiting for message

43+Sent ping

44+Received Hello!

45+Reply: Hello back!

46+94

47+Waiting for message

48+Sent ping

49+Received Hello!

50+Reply: Hello back!

51+93

52+Waiting for message

53+Sent ping

54+Received Hello!

55+Reply: Hello back!

56+92

57+Waiting for message

58+Sent ping

59+Received Hello!

60+Reply: Hello back!

61+91

62+Waiting for message

63+Sent ping

64+Received Hello!

65+Reply: Hello back!

66+90

67+Waiting for message

68+Sent ping

69+Received Hello!

70+Reply: Hello back!

71+89

72+Waiting for message

73+Sent ping

74+Received Hello!

75+Reply: Hello back!

76+88

77+Waiting for message

78+Sent ping

79+Received Hello!

80+Reply: Hello back!

81+87

82+Waiting for message

83+Sent ping

84+Received Hello!

85+Reply: Hello back!

86+86

87+Waiting for message

88+Sent ping

89+Received Hello!

90+Reply: Hello back!

91+85

92+Waiting for message

93+Sent ping

94+Received Hello!

95+Reply: Hello back!

96+84

97+Waiting for message

98+Sent ping

99+Received Hello!

100+Reply: Hello back!

101+83

102+Waiting for message

103+Sent ping

104+Received Hello!

105+Reply: Hello back!

106+82

107+Waiting for message

108+Sent ping

109+Received Hello!

110+Reply: Hello back!

111+81

112+Waiting for message

113+Sent ping

114+Received Hello!

115+Reply: Hello back!

116+80

117+Waiting for message

118+Sent ping

119+Received Hello!

120+Reply: Hello back!

121+79

122+Waiting for message

123+Sent ping

124+Received Hello!

125+Reply: Hello back!

126+78

127+Waiting for message

128+Sent ping

129+Received Hello!

130+Reply: Hello back!

131+77

132+Waiting for message

133+Sent ping

134+Received Hello!

135+Reply: Hello back!

136+76

137+Waiting for message

138+Sent ping

139+Received Hello!

140+Reply: Hello back!

141+75

142+Waiting for message

143+Sent ping

144+Received Hello!

145+Reply: Hello back!

146+74

147+Waiting for message

148+Sent ping

149+Received Hello!

150+Reply: Hello back!

151+73

152+Waiting for message

153+Sent ping

154+Received Hello!

155+Reply: Hello back!

156+72

157+Waiting for message

158+Sent ping

159+Received Hello!

160+Reply: Hello back!

161+71

162+Waiting for message

163+Sent ping

164+Received Hello!

165+Reply: Hello back!

166+70

167+Waiting for message

168+Sent ping

169+Received Hello!

170+Reply: Hello back!

171+69

172+Waiting for message

173+Sent ping

174+Received Hello!

175+Reply: Hello back!

176+68

177+Waiting for message

178+Sent ping

179+Received Hello!

180+Reply: Hello back!

181+67

182+Waiting for message

183+Sent ping

184+Received Hello!

185+Reply: Hello back!

186+66

187+Waiting for message

188+Sent ping

189+Received Hello!

190+Reply: Hello back!

191+65

192+Waiting for message

193+Sent ping

194+Received Hello!

195+Reply: Hello back!

196+64

197+Waiting for message

198+Sent ping

199+Received Hello!

200+Reply: Hello back!

201+63

202+Waiting for message

203+Sent ping

204+Received Hello!

205+Reply: Hello back!

206+62

207+Waiting for message

208+Sent ping

209+Received Hello!

210+Reply: Hello back!

211+61

212+Waiting for message

213+Sent ping

214+Received Hello!

215+Reply: Hello back!

216+60

217+Waiting for message

218+Sent ping

219+Received Hello!

220+Reply: Hello back!

221+59

222+Waiting for message

223+Sent ping

224+Received Hello!

225+Reply: Hello back!

226+58

227+Waiting for message

228+Sent ping

229+Received Hello!

230+Reply: Hello back!

231+57

232+Waiting for message

233+Sent ping

234+Received Hello!

235+Reply: Hello back!

236+56

237+Waiting for message

238+Sent ping

239+Received Hello!

240+Reply: Hello back!

241+55

242+Waiting for message

243+Sent ping

244+Received Hello!

245+Reply: Hello back!

246+54

247+Waiting for message

248+Sent ping

249+Received Hello!

250+Reply: Hello back!

251+53

252+Waiting for message

253+Sent ping

254+Received Hello!

255+Reply: Hello back!

256+52

257+Waiting for message

258+Sent ping

259+Received Hello!

260+Reply: Hello back!

261+51

262+Waiting for message

263+Sent ping

264+Received Hello!

265+Reply: Hello back!

266+50

267+Waiting for message

268+Sent ping

269+Received Hello!

270+Reply: Hello back!

271+49

272+Waiting for message

273+Sent ping

274+Received Hello!

275+Reply: Hello back!

276+48

277+Waiting for message

278+Sent ping

279+Received Hello!

280+Reply: Hello back!

281+47

282+Waiting for message

283+Sent ping

284+Received Hello!

285+Reply: Hello back!

286+46

287+Waiting for message

288+Sent ping

289+Received Hello!

290+Reply: Hello back!

291+45

292+Waiting for message

293+Sent ping

294+Received Hello!

295+Reply: Hello back!

296+44

297+Waiting for message

298+Sent ping

299+Received Hello!

300+Reply: Hello back!

301+43

302+Waiting for message

303+Sent ping

304+Received Hello!

305+Reply: Hello back!

306+42

307+Waiting for message

308+Sent ping

309+Received Hello!

310+Reply: Hello back!

311+41

312+Waiting for message

313+Sent ping

314+Received Hello!

315+Reply: Hello back!

316+40

317+Waiting for message

318+Sent ping

319+Received Hello!

320+Reply: Hello back!

321+39

322+Waiting for message

323+Sent ping

324+Received Hello!

325+Reply: Hello back!

326+38

327+Waiting for message

328+Sent ping

329+Received Hello!

330+Reply: Hello back!

331+37

332+Waiting for message

333+Sent ping

334+Received Hello!

335+Reply: Hello back!

336+36

337+Waiting for message

338+Sent ping

339+Received Hello!

340+Reply: Hello back!

341+35

342+Waiting for message

343+Sent ping

344+Received Hello!

345+Reply: Hello back!

346+34

347+Waiting for message

348+Sent ping

349+Received Hello!

350+Reply: Hello back!

351+33

352+Waiting for message

353+Sent ping

354+Received Hello!

355+Reply: Hello back!

356+32

357+Waiting for message

358+Sent ping

359+Received Hello!

360+Reply: Hello back!

361+31

362+Waiting for message

363+Sent ping

364+Received Hello!

365+Reply: Hello back!

366+30

367+Waiting for message

368+Sent ping

369+Received Hello!

370+Reply: Hello back!

371+29

372+Waiting for message

373+Sent ping

374+Received Hello!

375+Reply: Hello back!

376+28

377+Waiting for message

378+Sent ping

379+Received Hello!

380+Reply: Hello back!

381+27

382+Waiting for message

383+Sent ping

384+Received Hello!

385+Reply: Hello back!

386+26

387+Waiting for message

388+Sent ping

389+Received Hello!

390+Reply: Hello back!

391+25

392+Waiting for message

393+Sent ping

394+Received Hello!

395+Reply: Hello back!

396+24

397+Waiting for message

398+Sent ping

399+Received Hello!

400+Reply: Hello back!

401+23

402+Waiting for message

403+Sent ping

404+Received Hello!

405+Reply: Hello back!

406+22

407+Waiting for message

408+Sent ping

409+Received Hello!

410+Reply: Hello back!

411+21

412+Waiting for message

413+Sent ping

414+Received Hello!

415+Reply: Hello back!

416+20

417+Waiting for message

418+Sent ping

419+Received Hello!

420+Reply: Hello back!

421+19

422+Waiting for message

423+Sent ping

424+Received Hello!

425+Reply: Hello back!

426+18

427+Waiting for message

428+Sent ping

429+Received Hello!

430+Reply: Hello back!

431+17

432+Waiting for message

433+Sent ping

434+Received Hello!

435+Reply: Hello back!

436+16

437+Waiting for message

438+Sent ping

439+Received Hello!

440+Reply: Hello back!

441+15

442+Waiting for message

443+Sent ping

444+Received Hello!

445+Reply: Hello back!

446+14

447+Waiting for message

448+Sent ping

449+Received Hello!

450+Reply: Hello back!

451+13

452+Waiting for message

453+Sent ping

454+Received Hello!

455+Reply: Hello back!

456+12

457+Waiting for message

458+Sent ping

459+Received Hello!

460+Reply: Hello back!

461+11

462+Waiting for message

463+Sent ping

464+Received Hello!

465+Reply: Hello back!

466+10

467+Waiting for message

468+Sent ping

469+Received Hello!

470+Reply: Hello back!

471+9

472+Waiting for message

473+Sent ping

474+Received Hello!

475+Reply: Hello back!

476+8

477+Waiting for message

478+Sent ping

479+Received Hello!

480+Reply: Hello back!

481+7

482+Waiting for message

483+Sent ping

484+Received Hello!

485+Reply: Hello back!

486+6

487+Waiting for message

488+Sent ping

489+Received Hello!

490+Reply: Hello back!

491+5

492+Waiting for message

493+Sent ping

494+Received Hello!

495+Reply: Hello back!

496+4

497+Waiting for message

498+Sent ping

499+Received Hello!

500+Reply: Hello back!

501+3

502+Waiting for message

503+Sent ping

504+Received Hello!

505+Reply: Hello back!

506+2

507+Waiting for message

508+Sent ping

509+Received Hello!

510+Reply: Hello back!

511+1

512+Waiting for message

513+Sent ping

514+Received Hello!

515+Reply: Hello back!

test/test018/run+3−1

@@ -1,4 +1,6 @@

1#!/bin/bash

2idris test018.idr -o test018

3+idris test018a.idr -o test018a

3./test018

4./test018

5+./test018a

4−rm -f test018 *.ibc

6+rm -f test018 test018a *.ibc