[Caml-list] Type Safety and Interruptions

[Caml-list] Type Safety and Interruptions

[Oleg Trott]

Hi

Are there any guarantees about type safety even when program execution is 
interrupted?

As a simple example, suppose f is a function that modifies its argument 
(array) frequently, x is some value, and I type in the toplevel:


# (* ..... *)
#  let a = Array.make 100000 x;;
#  f a;;
Interrupted.


and interrupt it before f finishes. Is it at all possible for array "a" to 
be in some odd state when its `value' is inconsistent with its type?

What if "f" also contains calls to foreign (C/FORTRAN) functions?

Thanks in advance

-- 
Oleg Trott <oleg_trott@columbia.edu>

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Type Safety and Interruptions

[Xavier Leroy]

> Are there any guarantees about type safety even when program execution is 
> interrupted?

Yes.  Signals are not processed in a completely asynchronous manner.
Rather, they are recorded and processed later when the program reaches
a safe program point, e.g. not in the middle of an allocation, an
initialization, nor a GC.

> As a simple example, suppose f is a function that modifies its argument 
> (array) frequently, x is some value, and I type in the toplevel:
> 
> 
> # (* ..... *)
> #  let a = Array.make 100000 x;;
> #  f a;;
> Interrupted.
> 
> and interrupt it before f finishes. Is it at all possible for array "a" to 
> be in some odd state when its `value' is inconsistent with its type?

No, this cannot happen.  The array may be partially modified
(depending on what f did before being interrupted), but it will always
hold valid integers.

> What if "f" also contains calls to foreign (C/FORTRAN) functions?

Same thing.  By default, the signals are delayed till the foreign
function returns and the Caml program hits a safe point.  Some foreign
functions can explicitly declare a "blocking section" where they are
going to block for an unbounded amount of time, and within this
section signals will be processed immediately.  However, it is part of
the "blocking section" contract that the C function must not touch the
Caml heap as long as it is within the blocking section, so again heap
corruption cannot occur.

Hope this helps,

- Xavier Leroy

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners