* [Caml-list] Calling Java function from OCaml @ 2018-04-12 9:40 mukesh tiwari 2018-04-12 10:00 ` Gabriel Scherer 2018-04-12 18:57 ` forum 0 siblings, 2 replies; 6+ messages in thread From: mukesh tiwari @ 2018-04-12 9:40 UTC (permalink / raw) To: caml-list [-- Attachment #1: Type: text/plain, Size: 740 bytes --] Hi Everyone, I am trying to call some Java functions from OCaml (Extracted from Coq if it matters). I am familiar with ocamljava [1], but it says that "*The generated code usually runs faster than OCaml bytecode but slower than native code. Memory consumption and startup time are also higher, but leveraging the multiple cores of a machine can help reaching the performance level of native code.*", and I don't want to leave the OCaml native code. One suggestion I got on #ocaml channel is using RPC and a quick Google search leads to ocaml-rpc [2]. I am wondering if experts from OCaml community could please give me some suggestions. Best regards, Mukesh Tiwari [1] http://www.ocamljava.org/ [2] https://github.com/mirage/ocaml-rpc [-- Attachment #2: Type: text/html, Size: 967 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Calling Java function from OCaml 2018-04-12 9:40 [Caml-list] Calling Java function from OCaml mukesh tiwari @ 2018-04-12 10:00 ` Gabriel Scherer 2018-04-12 19:06 ` forum 2018-04-12 18:57 ` forum 1 sibling, 1 reply; 6+ messages in thread From: Gabriel Scherer @ 2018-04-12 10:00 UTC (permalink / raw) To: mukesh tiwari; +Cc: caml users [-- Attachment #1: Type: text/plain, Size: 2837 bytes --] Remote procedure calls are a generic solution to cross-language computations that works in many settings. It is a perfectly reasonable thing to do. Another option is to use Foreign Function Interfaces on both sides to do cross-language computation in a single system process (instead of RPCs and communicating processes). For Java, the FFI layer in the JNI (Java Native Interface), and there exists a library to make OCaml and Java functions communicate through the JNI (without changing the OCaml compilation backend): https://github.com/xavierleroy/camljava That said, this library seems to currently lack active users, and in particular nobody did the work of packaging it on opam ( https://github.com/ocaml/opam-repository/issues/7519 ). If you are willing to give this library a try, it could be a useful thing to contribute. In either cases, I would recommend being very careful in designing the interface between Coq code and untrusted code (pure OCaml, or OCaml+Java code using whichever coordination system). It is easy to shoot yourself in the foot by exporting untrusted functions with an optimistic type (eg. using the Coq function type for the untrusted functions that may not be total / strongly terminating). If you can design the interface between Coq and untrusted code as primarily based on exchanging ground *data* (events, queries reified as algebraic datatypes...), with an explicit loop orchestrating the coordination between both, you can get a system where the correctness guarantees (or lack thereof) are much easier to reason about. Incidentally, this design also makes the in-process data exchange more similar to what an inter-process communication system would look like, so it allows implement both solutions (in-process or remote communication) against a single Coq codebase, with minimal changes. (As an aside: the #ocaml channel is also populated by experts from the OCaml community, so its advice is probably as good as the list.) On Thu, Apr 12, 2018 at 11:40 AM, mukesh tiwari < mukeshtiwari.iiitm@gmail.com> wrote: > Hi Everyone, > I am trying to call some Java functions from OCaml (Extracted from Coq if > it matters). I am familiar with ocamljava [1], but it says that "*The > generated code usually runs faster than OCaml bytecode but slower than > native code. Memory consumption and startup time are also higher, but > leveraging the multiple cores of a machine can help reaching the > performance level of native code.*", and I don't want to leave the OCaml > native code. One suggestion I got on #ocaml channel is using RPC and a > quick Google search leads to ocaml-rpc [2]. I am wondering if experts from > OCaml community could please give me some suggestions. > > > Best regards, > Mukesh Tiwari > > > [1] http://www.ocamljava.org/ > [2] https://github.com/mirage/ocaml-rpc > [-- Attachment #2: Type: text/html, Size: 3661 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Calling Java function from OCaml 2018-04-12 10:00 ` Gabriel Scherer @ 2018-04-12 19:06 ` forum 0 siblings, 0 replies; 6+ messages in thread From: forum @ 2018-04-12 19:06 UTC (permalink / raw) To: Gabriel Scherer; +Cc: Xavier Clerc, mukesh tiwari, caml users > Le 12 avr. 2018 à 11:00, Gabriel Scherer <gabriel.scherer@gmail.com> a écrit : > > Remote procedure calls are a generic solution to cross-language computations that works in many settings. It is a perfectly reasonable thing to do. My (limited) experience led me to a sightly more nuanced conclusion. It decisively depends on the shape/size of the data to be exchanged. (Not that the granularity of computations does not matter...) Kind regards, Xavier Clerc ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Calling Java function from OCaml 2018-04-12 9:40 [Caml-list] Calling Java function from OCaml mukesh tiwari 2018-04-12 10:00 ` Gabriel Scherer @ 2018-04-12 18:57 ` forum 2018-04-13 3:01 ` mukesh tiwari 1 sibling, 1 reply; 6+ messages in thread From: forum @ 2018-04-12 18:57 UTC (permalink / raw) To: mukesh tiwari; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 1599 bytes --] > Le 12 avr. 2018 à 10:40, mukesh tiwari <mukeshtiwari.iiitm@gmail.com> a écrit : > > Hi Everyone, > I am trying to call some Java functions from OCaml (Extracted from Coq if it matters). I am familiar with ocamljava [1], but it says that "The generated code usually runs faster than OCaml bytecode but slower than native code. Memory consumption and startup time are also higher, but leveraging the multiple cores of a machine can help reaching the performance level of native code.", and I don't want to leave the OCaml native code. One suggestion I got on #ocaml channel is using RPC and a quick Google search leads to ocaml-rpc [2]. I am wondering if experts from OCaml community could please give me some suggestions. For the record, the performance of ocamljava-compiled code heavily depends on the programming style. Numerical imperative or i/o-bound code can be on par with ocamlopt-compiled code, while code based on exceptions for control flow or abundant indirect calls can be slower than ocamlc-compiled code. I am afraid extracted code is likely to fall in the second category. It is also noteworthy that you can run into problems with extracted code. I suspect extracted code might contain call to "Obj.magic", as the type system of Coq is slightly more powerful than the one of OCaml. The issue is that that OCaml-Java uses a different memory layout, so that "Obj.magic" might not yield the same result as in vanilla OCaml. Best regards, Xavier Clerc PS: if you are able to share your code, I might be able to give you a less generic assessment. [-- Attachment #2: Type: text/html, Size: 2425 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Calling Java function from OCaml 2018-04-12 18:57 ` forum @ 2018-04-13 3:01 ` mukesh tiwari 2018-04-15 18:26 ` forum 0 siblings, 1 reply; 6+ messages in thread From: mukesh tiwari @ 2018-04-13 3:01 UTC (permalink / raw) To: forum, caml-list [-- Attachment #1: Type: text/plain, Size: 3024 bytes --] Hi Xavier, and Gabriel, Thank you very much for reply. Let me give me general understanding of my project. I am trying to count encrypted ballots (Additive Elgamal) which is matrix of ciphertext. We multiply these ballots (matrices) point wise and decrypt it to get additive final value in plaintext [2]. For encryption, decryption and zero knowledge proof, we are using unicrypt library [3]. You can see the encryption part in Coq as Axiom [4] and will be realized by java functions from unicrypt library in extracted OCaml code [5]. We will replace the Z [6] with big_int in OCaml. I am also wondering if these things (unicrypt functionality of encryption, decryption and zero knowledge proof) can be realized by CertiCrypt [7] ? Best regards, Mukesh Tiwari [1] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/ballot_mat.txt [2] https://nvotes.com/multiplicative-vs-additive-homomorphic-elgamal/ [3] https://github.com/bfh-evg/unicrypt [4] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/EncryptionSchulze.v#L713 [5] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/lib.ml [6] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/lib.ml#L74 [7] https://github.com/EasyCrypt On Fri, Apr 13, 2018 at 4:57 AM, forum@x9c.fr <forum@x9c.fr> wrote: > > Le 12 avr. 2018 à 10:40, mukesh tiwari <mukeshtiwari.iiitm@gmail.com> a > écrit : > > Hi Everyone, > I am trying to call some Java functions from OCaml (Extracted from Coq if > it matters). I am familiar with ocamljava [1], but it says that "*The > generated code usually runs faster than OCaml bytecode but slower than > native code. Memory consumption and startup time are also higher, but > leveraging the multiple cores of a machine can help reaching the > performance level of native code.*", and I don't want to leave the OCaml > native code. One suggestion I got on #ocaml channel is using RPC and a > quick Google search leads to ocaml-rpc [2]. I am wondering if experts from > OCaml community could please give me some suggestions. > > > For the record, the performance of ocamljava-compiled code > heavily depends on the programming style. Numerical imperative > or i/o-bound code can be on par with ocamlopt-compiled code, > while code based on exceptions for control flow or abundant indirect > calls can be slower than ocamlc-compiled code. I am afraid > extracted code is likely to fall in the second category. > > It is also noteworthy that you can run into problems with extracted > code. I suspect extracted code might contain call to "Obj.magic", > as the type system of Coq is slightly more powerful than the one > of OCaml. The issue is that that OCaml-Java uses a different > memory layout, so that "Obj.magic" might not yield the same result > as in vanilla OCaml. > > > Best regards, > > Xavier Clerc > > PS: if you are able to share your code, I might be able to give you > a less generic assessment. > [-- Attachment #2: Type: text/html, Size: 4573 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Calling Java function from OCaml 2018-04-13 3:01 ` mukesh tiwari @ 2018-04-15 18:26 ` forum 0 siblings, 0 replies; 6+ messages in thread From: forum @ 2018-04-15 18:26 UTC (permalink / raw) To: mukesh tiwari; +Cc: Xavier Clerc, caml-list > Le 13 avr. 2018 à 04:01, mukesh tiwari <mukeshtiwari.iiitm@gmail.com> a écrit : > > Hi Xavier, and Gabriel, > Thank you very much for reply. Let me give me general understanding of my project. I am trying to count encrypted ballots (Additive Elgamal) which is matrix of ciphertext. We multiply these ballots (matrices) point wise and decrypt it to get additive final value in plaintext [2]. For encryption, decryption and zero knowledge proof, we are using unicrypt library [3]. You can see the encryption part in Coq as Axiom [4] and will be realized by java functions from unicrypt library in extracted OCaml code [5]. We will replace the Z [6] with big_int in OCaml. Thanks for sharing the details. I am afraid OCaml-Java might not be a good fit, for at least two (related) reasons: - the implementation of `big_int` that ships with OCaml-Java has been very lightly tested, and I would not be surprised if it turned out to be buggy; - if you do not replace type `z` with `big_int` your code will be unbearably slow (it, of course, applies to both ocamlopt- and ocamljava-compiled code, but the price of allocating short-lived object is significantly higher on the JVM). Obviously, another possibility would be to use BigIntegers from the JDK [1]. It looks like the class contains all the primitives you need (I only skimmed over `lib.ml`, though). Best regards, Xavier Clerc [1] https://docs.oracle.com/javase/7/docs/api/java/math/BigInteger.html ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2018-04-15 18:26 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-04-12 9:40 [Caml-list] Calling Java function from OCaml mukesh tiwari 2018-04-12 10:00 ` Gabriel Scherer 2018-04-12 19:06 ` forum 2018-04-12 18:57 ` forum 2018-04-13 3:01 ` mukesh tiwari 2018-04-15 18:26 ` forum
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox