Segfault in sandmark frama-c

[sadiqj]

If you check out the bugfix/ctk21/frama-c-multicore-effects branch from @ctk21 on https://github.com/ocamllabs/sandmark and start a run with multicore the built frama-c segfaults.

Backtrace:

#1  0x00005555562e13db in scan_native_globals (fdata=0x0, f=0x5555562c9ea0 <caml_darken>)
   at globroots.c:177
#2  caml_scan_global_roots (f=f@entry=0x5555562c9ea0 <caml_darken>, fdata=fdata@entry=0x0)
   at globroots.c:199
#3  0x00005555562c800a in caml_do_roots (f=f@entry=0x5555562c9ea0 <caml_darken>, fdata=fdata@entry=0x0,
   d=d@entry=0x555556ba4410 <all_domains+16>, do_final_val=do_final_val@entry=0) at roots.c:52
#4  0x00005555562ca760 in cycle_all_domains_callback (domain=0x555556ba4410 <all_domains+16>,
   unused=unused@entry=0x0) at major_gc.c:891
#5  0x00005555562e5537 in caml_try_run_on_all_domains (
   handler=handler@entry=0x5555562ca610 <cycle_all_domains_callback>, data=data@entry=0x0)
   at domain.c:545
#6  0x00005555562cb07a in major_collection_slice (howmuch=howmuch@entry=0,
   from_barrier=from_barrier@entry=0, budget_left=budget_left@entry=0x0) at major_gc.c:1135
#7  0x00005555562cb1ea in caml_major_collection_slice (howmuch=howmuch@entry=0,
   budget_left=budget_left@entry=0x0) at major_gc.c:1147
#8  0x00005555562cc612 in caml_minor_collection () at minor_gc.c:705
#9  0x00005555562d322a in caml_make_vect (len=<optimised out>, init=<optimised out>) at array.c:312
#10 <signal handler called>
#11 0x0000555556036e34 in camlHptmap__cached_fold_5067 () at src/libraries/utils/hptmap.ml:1420
#12 0x00007fffef82eec0 in camlEva__Equality__entry ()
   at src/plugins/value/domains/equality/equality.ml:409
#13 <signal handler called>
#14 caml_callback (closure=closure@entry=140737488345256, arg=arg@entry=0) at callback.c:176
#15 0x00005555562e2bc8 in caml_natdynlink_run (handle_v=<optimised out>, symbol=<optimised out>)
   at natdynlink.c:139
#16 <signal handler called>
#17 0x000055555614f4e7 in camlDynlink__fun_1880 () at otherlibs/dynlink/natdynlink.ml:186
#18 0x000055555623588f in camlList__iter_1083 () at list.ml:100
#19 0x000055555614f2ff in camlDynlink__loadunits_1595 () at otherlibs/dynlink/natdynlink.ml:186
#20 0x000055555614f575 in camlDynlink__load_1608 () at otherlibs/dynlink/natdynlink.ml:192
#21 0x0000555555ff5d7f in camlDynamic__dynlib_module_1566 () at otherlibs/dynlink/natdynlink.ml:195
#22 0x000055555623588f in camlList__iter_1083 () at list.ml:100
#23 0x000055555623588f in camlList__iter_1083 () at list.ml:100
#24 0x0000555555ff67be in camlDynamic__load_packages_1792 ()
   at src/kernel_services/plugin_entry_points/dynamic.ml:158
#25 0x0000555555fae639 in camlKernel__bootstrap_loader_10507 ()
   at src/kernel_services/plugin_entry_points/kernel.ml:761
#26 0x00005555560b869d in camlCmdline__parse_and_boot_2266 ()
   at src/kernel_services/cmdline_parameters/cmdline.ml:836
#27 0x00005555560b4932 in camlCmdline__catch_toplevel_run_1648 ()
   at src/kernel_services/cmdline_parameters/cmdline.ml:229
#28 0x0000555555bf18f8 in camlBoot__entry () at src/kernel_internals/runtime/boot.ml:72
#29 0x0000555555be9c7b in caml_program ()
#30 <signal handler called>
#31 caml_startup_common (argv=0x7fffffffdaf8, pooling=<optimised out>, pooling@entry=0) at startup.c:137
#32 0x00005555562e8d58 in caml_startup_exn (argv=<optimised out>) at startup.c:141
#33 caml_main (argv=<optimised out>) at startup.c:146
#34 0x0000555555be893c in main (argc=<optimised out>, argv=<optimised out>) at main.c:44```

_Note - don't forget to follow the instruction on the README in that branch for replacing the ctypes dependency with a multicore compatible one_

[anmolsahoo25]

At

ocaml-multicore/byterun/major_gc.c

Lines 605 to 610 in 8fbacb1

	atomic_store_explicit(
	Hp_atomic_val(v),
	With_status_hd(hd, global.MARKED),
	memory_order_relaxed);
	if (Tag_hd(hd) < No_scan_tag) {
	mark_entry e = {v, 0, Wosize_val(v)};

,

there is a store to caml_int64_ops - 8, since this memory area is read-only, it raises a segmentation fault.

[kayceesrk]

Frama-C assumes that it is compiled with naked-pointer support [0]. Multicore does not support naked pointers, nor does vanilla OCaml compiled with -no-naked-pointers. The solution is to fix Frama-C upstream. This bug won't be fixed here.

[0] https://github.com/Frama-C/Frama-C-snapshot/blob/2f7a0eee0a8083374236da6a59a8d500de00305d/src/libraries/datatype/unmarshal.ml#L72-L73

[mshinwell]

I think you can just allow zero as a distinguished null value, which is the current plan for upstream no-naked pointers, as I mentioned elsewhere. This is a small fix in the runtime, which I would suggest you make, so you can run these benchmarks.

[kayceesrk]

Do you mean to add Obj.null as a new feature? If the null need not be portable across runs, it would be easier to do something like https://github.com/ocaml-multicore/ocaml-multicore/blob/master/byterun/weak.c#L31-L34. Is this what you have in mind?

[mshinwell]

I was planning for it to be a compile-time constant, so it can also be a compile-time constant in C stubs, and comparison against it is fast.

[stedolan]

While this sounds good, Frama-C really does need to be fixed. Frama-C is attempting to get an all-bits-zero null value by loading a word from 0L : int64, but it loads the wrong word and gets a naked pointer to caml_int64_ops. (The value of an int64 is stored in the second word).

[kayceesrk]

Didn't realize that Frama-C was loading the wrong field!