Hi Kofi,

Thanks for your input. It actually solved my problem by just changing the config.

But, I ran into another problem with freeing an array, allocated using malloc.

Here's my simple code:

// In root thread/process

char *buf = malloc(409600);

// do sth with buf

free(buf); // here I got an error saying "libsel4muslcsys: Error attempting syscall 91"

printf("done\n") // this one was printed out too

Does this have anything to do with config as well? I tried to increase malloc limit (which I dont think it's related much to free) but I still get an error. Also, no error was output if when I tried 4096 bytes as a size of buf.

Thanks, Oak

On Mon, Jul 18, 2016 at 6:33 PM, Norrathep Rattanavipanon nrattana@uci.edu wrote:

Hi,

So I followed hello-4 example. I can create a static array inside a second process (hello-4-app) and the second process works fine. However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work.

Any help would be appreciated.

Thanks,

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine