Reseña: Mutual exclusion by four shared bits with not more than quadratic complexity

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.

Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).

Su resumen es

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.

El código de las correspondientes teorías en PVS se encuentra aquí.

Reseña: Bind induction: Extracting monadic programs from proofs

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Bind induction: Extracting monadic programs from proofs.

Sus autores son Hadi Shafei y James Caldwell (de la Univ. de Wyoming).

Su resumen es

Container types can be modeled as foldable monads that support the MonadPlus operations together with a membership operation. In this paper we present a new typeclass we call -Monad that supports a membership operator for instances of the MonadPlus typeclass. The laws for the -Monad typeclass specify how membership behaves with respect to the monad and monad plus operators. Using -Monads we are able write specifications of properties of generic containers. We also present an induction rule for monads we call bind induction. The new proof rule is proved to be sound. The computational content of the new induction rule is a bind operator, using this rule we are able to extract monadic programs from proofs. We present an example that uses the rule to extract a monadic program from a proof of a specification. We have used the Coq theorem prover to formalize the definitions presented here and to prove properties of the formalization. We rely on the Coq Type Class mechanism for our formalization.

El trabajo se ha presentado en el Symposium on Trends in Functional Programming 2014.

El código de las correspondientes teorías en Coq se encuentra en epsilon-Monad.v y decomposition.v.

Reseña: HOCore in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado HOCore in Coq.

Sus autores son

Su resumen es

We consider a recent publication on higher-order process calculi and describe how its results are formalized in the Coq proof assistant. We also highlight some important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration, and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.

El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).

El código de las correspondientes teorías en Coq se encuentra aquí.

Reseña: Depth-first search and strong connectivity in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre grafos titulado Depth-first search and strong connectivity in Coq.

Su autor es François Pottier (del grupo Gallium en el INRIA de Rocquencourt).

Su resumen es

Using Coq, we mechanize Wegener’s proof of Kosaraju’s linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.

El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).

El código de las correspondientes teorías en Coq se encuentra aquí.