Comunicar procesos secuenciales

Modelo formal en la teoría de la concurrencia

En informática , la comunicación de procesos secuenciales ( CSP ) es un lenguaje formal para describir patrones de interacción en sistemas concurrentes . ^[1] Es un miembro de la familia de teorías matemáticas de concurrencia conocidas como álgebras de procesos o cálculos de procesos , basadas en el paso de mensajes a través de canales . CSP fue muy influyente en el diseño del lenguaje de programación occam ^{[1] [2]} y también influyó en el diseño de lenguajes de programación como Limbo , ^[3] RaftLib , Erlang , ^[4] Go , ^{[5] [3]} Crystal y core.async de Clojure . ^[6]

La CSP fue descrita por primera vez en un artículo de 1978 por Tony Hoare , ^[7] pero desde entonces ha evolucionado sustancialmente. ^[8] La CSP se ha aplicado prácticamente en la industria como una herramienta para especificar y verificar los aspectos concurrentes de una variedad de sistemas diferentes, como el T9000 Transputer , ^[9] así como un sistema de comercio electrónico seguro. ^[10] La teoría de la CSP en sí misma también sigue siendo objeto de investigación activa, incluido el trabajo para aumentar su rango de aplicabilidad práctica (por ejemplo, aumentando la escala de los sistemas que se pueden analizar de manera manejable). ^[11]

Historia

La versión de CSP presentada en el artículo original de Hoare de 1978 era esencialmente un lenguaje de programación concurrente en lugar de un cálculo de procesos . Tenía una sintaxis sustancialmente diferente a las versiones posteriores de CSP, no poseía una semántica definida matemáticamente ^[12] y no podía representar el no determinismo ilimitado ^[13] . Los programas en el CSP original se escribieron como una composición paralela de un número fijo de procesos secuenciales que se comunicaban entre sí estrictamente a través del paso de mensajes sincrónicos. A diferencia de las versiones posteriores de CSP, a cada proceso se le asignaba un nombre explícito y la fuente o el destino de un mensaje se definía especificando el nombre del proceso de envío o recepción previsto. Por ejemplo, el proceso

COPIA = *[c:carácter; oeste?c → este!c]

recibe repetidamente un carácter del proceso denominado westy envía ese carácter al proceso denominado east. La composición paralela

[oeste::DESMONTAR || X::COPIAR || este::MONTAR]

asigna los nombres westal DISASSEMBLEproceso, Xal COPYproceso y eastal ASSEMBLEproceso, y ejecuta estos tres procesos simultáneamente. ^[7]

Tras la publicación de la versión original de CSP, Hoare, Stephen Brookes y AW Roscoe desarrollaron y refinaron la teoría de CSP en su forma algebraica de procesos moderna. El enfoque adoptado para desarrollar CSP en un álgebra de procesos estuvo influenciado por el trabajo de Robin Milner sobre el Cálculo de sistemas de comunicación (CCS) y viceversa. La versión teórica de CSP se presentó inicialmente en un artículo de 1984 de Brookes, Hoare y Roscoe, ^[14] y más tarde en el libro de Hoare Communicating Sequential Processes , ^[12] que se publicó en 1985. En septiembre de 2006, ese libro seguía siendo la tercera referencia de informática más citada de todos los tiempos según Citeseer ^{[ cita requerida ]} (aunque una fuente poco confiable debido a la naturaleza de su muestreo). La teoría de CSP ha sufrido algunos cambios menores desde la publicación del libro de Hoare. La mayoría de estos cambios fueron motivados por la aparición de herramientas automatizadas para el análisis y la verificación de procesos de CSP. En The Theory and Practice of Concurrency ^[1] de Roscoe se describe esta nueva versión de CSP.

Aplicaciones

Una aplicación temprana e importante de CSP fue su uso para la especificación y verificación de elementos del Transputer INMOS T9000 , un procesador superescalar en pipeline complejo diseñado para soportar multiprocesamiento a gran escala. CSP se empleó para verificar la corrección tanto del pipeline del procesador como del Procesador de Canal Virtual, que administraba las comunicaciones fuera del chip para el procesador. ^[9]

La aplicación industrial de CSP al diseño de software se ha centrado habitualmente en sistemas fiables y críticos para la seguridad. Por ejemplo, el Bremen Institute for Safe Systems y Daimler-Benz Aerospace modelaron un sistema de gestión de fallos y una interfaz de aviónica (que consta de unas 23.000 líneas de código) destinados a su uso en la Estación Espacial Internacional en CSP, y analizaron el modelo para confirmar que su diseño estaba libre de bloqueos y bloqueos activos . ^{[15] [16]} El proceso de modelado y análisis fue capaz de descubrir una serie de errores que habrían sido difíciles de detectar utilizando únicamente pruebas. De forma similar, Praxis High Integrity Systems aplicó el modelado y análisis de CSP durante el desarrollo de software (aproximadamente 100.000 líneas de código) para una autoridad de certificación de tarjetas inteligentes seguras para verificar que su diseño era seguro y libre de bloqueos. Praxis afirma que el sistema tiene una tasa de defectos mucho menor que los sistemas comparables. ^[10]

Dado que el CSP es muy adecuado para modelar y analizar sistemas que incorporan intercambios de mensajes complejos, también se ha aplicado a la verificación de protocolos de comunicaciones y seguridad. Un ejemplo destacado de este tipo de aplicación es el uso que Lowe hizo del CSP y del verificador de refinamiento FDR para descubrir un ataque previamente desconocido al protocolo de autenticación de clave pública Needham-Schroeder y luego desarrollar un protocolo corregido capaz de derrotar el ataque. ^[17]

Descripción informal

Como sugiere su nombre, CSP permite la descripción de sistemas en términos de procesos componentes que operan de forma independiente e interactúan entre sí únicamente a través de la comunicación mediante el paso de mensajes . Sin embargo, la parte "secuencial" del nombre CSP es ahora un nombre poco apropiado, ya que el CSP moderno permite definir los procesos componentes como procesos secuenciales y como la composición paralela de procesos más primitivos. Las relaciones entre los diferentes procesos y la forma en que cada proceso se comunica con su entorno se describen utilizando varios operadores algebraicos de procesos . Con este enfoque algebraico, se pueden construir fácilmente descripciones de procesos bastante complejas a partir de unos pocos elementos primitivos.

Primitivos

CSP proporciona dos clases de primitivos en su álgebra de procesos:

Eventos

Los eventos representan comunicaciones o interacciones. Se supone que son indivisibles e instantáneos. Pueden ser nombres atómicos (por ejemplo, on , off ), nombres compuestos (por ejemplo, valve.open , valve.close ) o eventos de entrada/salida (por ejemplo, mouse?xy , screen!bitmap ).

Procesos primitivos

Los procesos primitivos representan comportamientos fundamentales: algunos ejemplos son STOP (el proceso que no comunica nada) y SKIP (que representa la finalización exitosa).

Operadores algebraicos

CSP tiene una amplia gama de operadores algebraicos. Los principales son:

Prefijo

El operador prefijo combina un evento y un proceso para producir un nuevo proceso. Por ejemplo, es el proceso que desea comunicar a con su entorno y, después de a , se comporta como el proceso P . $${\displaystyle a\to P}$$

Elección determinista

El operador de elección determinista (o externo) permite definir la evolución futura de un proceso como una elección entre dos procesos componentes y permite que el entorno resuelva la elección comunicando un evento inicial para uno de los procesos. Por ejemplo, es el proceso que está dispuesto a comunicar los eventos iniciales a y b y posteriormente se comporta como P o Q , dependiendo de qué evento inicial elija comunicar el entorno. Si tanto a como b se comunicaran simultáneamente, la elección se resolvería de manera no determinista. $${\displaystyle (a\to P)\Box (b\to Q)}$$

Elección no determinista

El operador de elección no determinista (o interno) permite definir la evolución futura de un proceso como una elección entre dos procesos componentes, pero no permite al entorno ningún control sobre cuál de los procesos componentes será seleccionado. Por ejemplo, puede comportarse como o . Puede negarse a aceptar a o b y solo está obligado a comunicarse si el entorno ofrece tanto a como b . El no determinismo puede introducirse inadvertidamente en una elección nominalmente determinista si los eventos iniciales de ambos lados de la elección son idénticos. Así, por ejemplo, es equivalente a $${\displaystyle (a\to P)\sqcap (b\to Q)}$$ ${\displaystyle (a\to P)}$ ${\displaystyle (b\to Q)}$ $${\displaystyle (a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})}$$ $${\displaystyle a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}}$$

Entrelazado

El operador de intercalación representa una actividad concurrente completamente independiente. El proceso se comporta como P y Q simultáneamente. Los eventos de ambos procesos se intercalan arbitrariamente en el tiempo. $${\displaystyle P\;|||\;Q}$$

Interfaz paralela

El operador paralelo de interfaz representa una actividad concurrente que requiere sincronización entre los procesos componentes: cualquier evento en el conjunto de interfaz solo puede ocurrir cuando todos los procesos componentes pueden participar en ese evento. Por ejemplo, el proceso requiere que P y Q puedan realizar el evento a antes de que ese evento pueda ocurrir. Entonces, por ejemplo, el proceso puede participar en el evento a y convertirse en el proceso mientras que simplemente se bloqueará. $${\displaystyle P\;|[\{a\}]|\;Q}$$ $${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$$ $${\displaystyle P\;|[\{a\}]|\;Q}$$ $${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$$

Ocultación

El operador de ocultación proporciona una forma de abstraer procesos haciendo que algunos eventos no sean observables. Un ejemplo trivial de ocultación es el que, suponiendo que el evento a no aparece en P , simplemente se reduce a $${\displaystyle (a\to P)\setminus \{a\}}$$ $${\displaystyle P}$$

Ejemplos

Uno de los ejemplos arquetípicos de CSP es una representación abstracta de una máquina expendedora de chocolate y sus interacciones con una persona que desea comprar chocolate. Esta máquina expendedora podría ser capaz de llevar a cabo dos eventos diferentes, “coin” y “choc”, que representan la inserción de un pago y la entrega de un chocolate respectivamente. Una máquina que exige un pago (solo en efectivo) antes de ofrecer un chocolate se puede escribir como:

$${\displaystyle \mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

Una persona que opte por utilizar una moneda o una tarjeta para realizar pagos podría modelarse como:

$${\displaystyle \mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )}$$

Estos dos procesos pueden ponerse en paralelo, de modo que puedan interactuar entre sí. El comportamiento del proceso compuesto depende de los eventos en los que los dos procesos componentes deben sincronizarse. Por lo tanto,

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

Mientras que si la sincronización sólo fuera necesaria en “moneda”, obtendríamos

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)}$$

Si abstraemos este último proceso compuesto ocultando los eventos “moneda” y “tarjeta”, es decir

$${\displaystyle \left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}}$$

obtenemos el proceso no determinista

$${\displaystyle \left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP} }$$

Se trata de un proceso que ofrece un evento “choc” y luego se detiene, o simplemente se detiene. En otras palabras, si tratamos la abstracción como una visión externa del sistema (por ejemplo, alguien que no ve la decisión tomada por la persona), se ha introducido el no determinismo .

Definición formal

Sintaxis

La sintaxis de CSP define las formas “legales” en las que se pueden combinar procesos y eventos. Sea e un evento y X un conjunto de eventos. Entonces, la sintaxis básica de CSP se puede definir como:

$${\displaystyle {\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc};{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}}$$

Tenga en cuenta que, en aras de la brevedad, la sintaxis presentada anteriormente omite el proceso que representa la divergencia , así como varios operadores como el paralelo alfabetizado, la canalización y las opciones indexadas. ${\displaystyle \mathbf {div} }$

Semántica formal

La CSP se ha imbuido de varias semánticas formales diferentes , que definen el significado de expresiones CSP sintácticamente correctas. La teoría de la CSP incluye semántica denotacional , semántica algebraica y semántica operacional mutuamente consistentes .

Semántica denotacional

Los tres modelos denotacionales principales de CSP son el modelo de trazas , el modelo de fallas estables y el modelo de fallas/divergencias . Las asignaciones semánticas de las expresiones de proceso a cada uno de estos tres modelos proporcionan la semántica denotacional para CSP. ^[1]

El modelo de trazas define el significado de una expresión de proceso como el conjunto de secuencias de eventos (trazas) que se puede observar que el proceso ejecuta. Por ejemplo,

• ${\displaystyle \mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}}$ya que no realiza ningún evento ${\displaystyle \mathrm {STOP} }$
• ${\displaystyle \mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}}$Dado que se puede observar que el proceso no ha realizado eventos, el evento a , o la secuencia de eventos a seguido de b ${\displaystyle (a\rightarrow b\rightarrow \mathrm {STOP} )}$

Más formalmente, el significado de un proceso P en el modelo de trazas se define como tal que: ${\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}$

1. ${\displaystyle \langle \rangle \in \mathrm {traces} \left(P\right)}$(es decir, contiene la secuencia vacía) ${\displaystyle \mathrm {traces} \left(P\right)}$
2. ${\displaystyle s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)}$(es decir, está cerrado por prefijo) ${\displaystyle \mathrm {traces} \left(P\right)}$

donde es el conjunto de todas las posibles secuencias finitas de eventos. ${\displaystyle \Sigma ^{\ast }}$

El modelo de fallas estables extiende el modelo de trazas con conjuntos de rechazo, que son conjuntos de eventos que un proceso puede negarse a realizar. Una falla es un par , que consiste en una traza s y un conjunto de rechazo X que identifica los eventos que un proceso puede rechazar una vez que ha ejecutado la traza s . El comportamiento observado de un proceso en el modelo de fallas estables se describe mediante el par . Por ejemplo, ${\displaystyle X\subseteq \Sigma }$ ${\displaystyle \left(s,X\right)}$ ${\displaystyle \left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)}$

$${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\Box \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}$$ $${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\sqcap \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}$$

El modelo de fallas/divergencias extiende aún más el modelo de fallas para manejar la divergencia . La semántica de un proceso en el modelo de fallas/divergencias es un par donde se define como el conjunto de todos los rastros que pueden conducir a un comportamiento divergente y . ${\displaystyle \left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)}$ ${\displaystyle \mathrm {divergences} \left(P\right)}$ ${\displaystyle \mathrm {failures} _{\perp }\left(P\right)=\mathrm {failures} \left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm {divergences} \left(P\right)\right\}}$

Herramientas

A lo largo de los años, se han producido varias herramientas para analizar y comprender los sistemas descritos mediante CSP. Las primeras implementaciones de herramientas utilizaban una variedad de sintaxis legibles por máquina para CSP, lo que hacía que los archivos de entrada escritos para diferentes herramientas fueran incompatibles. Sin embargo, la mayoría de las herramientas CSP ahora se han estandarizado en el dialecto legible por máquina de CSP ideado por Bryan Scattergood, a veces denominado CSP M. _[ ^18] El dialecto CSP _M de CSP posee una semántica operacional definida formalmente , que incluye un lenguaje de programación funcional integrado .

La herramienta CSP más conocida es probablemente Failures/Divergence Refinement 2 ( FDR2 ), que es un producto comercial desarrollado por Formal Systems (Europe) Ltd. FDR2 se describe a menudo como un verificador de modelos , pero técnicamente es un verificador de refinamiento , ya que convierte dos expresiones de proceso CSP en sistemas de transición etiquetados (LTS), y luego determina si uno de los procesos es un refinamiento del otro dentro de algún modelo semántico especificado (rastros, fallos o fallos/divergencia). ^[19] FDR2 aplica varios algoritmos de compresión de espacio de estado a los LTS de proceso para reducir el tamaño del espacio de estado que debe explorarse durante una verificación de refinamiento. FDR2 ha sido reemplazado por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, ejecución paralela y un verificador de tipos integrado. Fue publicado por la Universidad de Oxford, que también publicó FDR2 en el período 2008-12. ^[20]

El verificador de refinamiento de Adelaide ( ARC ) ^[21] es un verificador de refinamiento de CSP desarrollado por el Grupo de modelado y verificación formal de la Universidad de Adelaide . ARC se diferencia de FDR2 en que representa internamente los procesos de CSP como diagramas de decisión binaria ordenados (OBDD), lo que alivia el problema de explosión de estados de las representaciones LTS explícitas sin requerir el uso de algoritmos de compresión de espacio de estados como los utilizados en FDR2.

El proyecto ProB , ^[22] que está auspiciado por el Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, fue creado originalmente para respaldar el análisis de especificaciones construidas en el método B. Sin embargo, también incluye soporte para el análisis de procesos CSP tanto a través de la verificación de refinamiento como de la verificación de modelos LTL . ProB también se puede utilizar para verificar las propiedades de especificaciones CSP y B combinadas. Un ProBE CSP Animator está integrado en FDR3.

El kit de herramientas de análisis de procesos (PAT) ^{[23] [24]} es una herramienta de análisis de CSP desarrollada en la Escuela de Informática de la Universidad Nacional de Singapur . PAT puede realizar comprobaciones de refinamiento, comprobaciones de modelos LTL y simulación de procesos CSP y CSP temporizado. El lenguaje de proceso PAT extiende CSP con soporte para variables compartidas mutables, paso de mensajes asincrónico y una variedad de construcciones de procesos relacionados con el tiempo cuantitativo y de equidad, como deadliney waituntil. El principio de diseño subyacente del lenguaje de proceso PAT es combinar un lenguaje de especificación de alto nivel con programas procedimentales (por ejemplo, un evento en PAT puede ser un programa secuencial o incluso una llamada a una biblioteca externa de C#) para una mayor expresividad. Las variables compartidas mutables y los canales asincrónicos proporcionan un azúcar sintáctico conveniente para los patrones de modelado de procesos bien conocidos que se utilizan en CSP estándar. La sintaxis PAT es similar, pero no idéntica, a CSP _M . ^{[25] Las principales diferencias entre la sintaxis PAT y la CSP} _M estándar son el uso de punto y coma para terminar expresiones de proceso, la inclusión de azúcar sintáctica para variables y asignaciones, y el uso de una sintaxis ligeramente diferente para la elección interna y la composición paralela.

VisualNets ^[26] produce visualizaciones animadas de sistemas CSP a partir de especificaciones y admite CSP cronometrado.

CSPsim ^[27] es un simulador perezoso. No modela la verificación de CSP, pero es útil para explorar sistemas muy grandes (potencialmente infinitos).

SyncStitch es un verificador de refinamiento de CSP con un entorno de análisis y modelado interactivo. Tiene un editor gráfico de diagramas de transición de estado. El usuario puede modelar el comportamiento de los procesos no solo como expresiones de CSP sino también como diagramas de transición de estado. El resultado de la verificación también se informa gráficamente como árboles de cálculo y se puede analizar de forma interactiva con herramientas de inspección periféricas. Además de las verificaciones de refinamiento, puede realizar verificaciones de bloqueos y de bloqueos activos.

Formalismos relacionados

Varios otros lenguajes de especificación y formalismos se han derivado del clásico CSP no cronometrado o se han inspirado en él, entre ellos:

• CSP temporizado ^{[ enlace muerto permanente ]} , que incorpora información de tiempo para razonar sobre sistemas en tiempo real
• Teoría del proceso receptivo, una especialización de CSP que supone una operación de envío asincrónica (es decir, sin bloqueo )
• CSP
• Programa de salud pública
• TCOZ, una integración de Timed CSP y Object Z
• Circus, una integración de CSP y Z basada en las Teorías Unificadoras de Programación
• CML Archivado el 19 de febrero de 2020 en Wayback Machine (lenguaje de modelado COMPASS), una combinación de Circus y VDM desarrollada para el modelado de sistemas de sistemas (SoS)
• CspCASL, una extensión de CASL que integra CSP
• LOTOS , un estándar internacional ^[28] que incorpora características de CSP y CCS .
• PALPS, una extensión probabilística con ubicaciones para modelos ecológicos desarrollada por Anna Philippou y Mauricio Toro Bermúdez

Comparación con el modelo de actor

En la medida en que se relaciona con procesos concurrentes que intercambian mensajes, el modelo de actor es muy similar al CSP. Sin embargo, los dos modelos toman algunas decisiones fundamentalmente diferentes con respecto a los primitivos que proporcionan:

• Los procesos de CSP son anónimos, mientras que los actores tienen identidades.
• El CSP utiliza canales explícitos para el paso de mensajes, mientras que los sistemas de actores transmiten mensajes a actores de destino designados. Estos enfoques pueden considerarse duales entre sí, en el sentido de que los procesos que reciben a través de un único canal tienen efectivamente una identidad correspondiente a ese canal, mientras que el acoplamiento basado en nombres entre actores puede romperse mediante la construcción de actores que se comporten como canales.
• El paso de mensajes CSP implica fundamentalmente un encuentro entre los procesos implicados en el envío y la recepción del mensaje, es decir, el remitente no puede transmitir un mensaje hasta que el receptor esté listo para aceptarlo. Por el contrario, el paso de mensajes en sistemas de actores es fundamentalmente asincrónico, es decir, la transmisión y la recepción de mensajes no tienen que ocurrir al mismo tiempo, y los remitentes pueden transmitir mensajes antes de que los receptores estén listos para aceptarlos. Estos enfoques también pueden considerarse duales entre sí, en el sentido de que los sistemas basados ​​en encuentros pueden usarse para construir comunicaciones con búfer que se comporten como sistemas de mensajería asincrónicos, mientras que los sistemas asincrónicos pueden usarse para construir comunicaciones de estilo encuentro mediante el uso de un protocolo de mensaje/acuse de recibo para sincronizar remitentes y receptores.

Tenga en cuenta que las propiedades mencionadas anteriormente no necesariamente hacen referencia al documento original de CSP de Hoare, sino más bien a la encarnación moderna de la idea, como se ve en implementaciones como Go y core.async de Clojure. En el documento original, los canales no eran una parte central de la especificación y los procesos de envío y recepción en realidad se identifican entre sí por su nombre.

Otorgar

En 1990, “ se otorgó un Premio de la Reina por Logros Tecnológicos... al Laboratorio de Computación de la [Universidad de Oxford] . El premio reconoce una colaboración exitosa entre el laboratorio e Inmos Ltd. … El producto estrella de Inmos es el ' transputer ', un microprocesador con muchas de las partes que normalmente se necesitarían además integradas en el mismo componente único ”. ^[29] Según Tony Hoare, ^[30] “El Transputer de INMOS fue la encarnación de las ideas… de construir microprocesadores que pudieran comunicarse entre sí a través de cables que se extenderían entre sus terminales. El fundador tuvo la visión de que las ideas de CSP estaban maduras para la explotación industrial, y las convirtió en la base del lenguaje para programar Transputers, que se llamó Occam . … La compañía estimó que les permitió entregar el hardware un año antes de lo que hubiera sucedido de otra manera. Solicitaron y ganaron un premio de la Reina por logros tecnológicos, en conjunto con el Laboratorio de Computación de la Universidad de Oxford”.

Véase también

• Teoría de las trazas , teoría general de las trazas.
• Monoide de traza y monoide de historial
• Lenguaje de programación fácil
• Lenguaje de programación XC
• VerilogCSP es un conjunto de macros agregadas a Verilog HDL para respaldar la comunicación de canales de procesos secuenciales.
• Joyce es un lenguaje de programación basado en los principios de CSP, desarrollado por Brinch Hansen alrededor de 1989.
• SuperPascal es un lenguaje de programación también desarrollado por Brinch Hansen , influenciado por CSP y su trabajo anterior con Joyce .
• Ada implementa características de CSP como el encuentro.
• DirectShow es el marco de video dentro de DirectX , utiliza los conceptos CSP para implementar los filtros de audio y video.
• OpenComRTOS es un RTOS distribuido centrado en la red desarrollado formalmente basado en un superconjunto pragmático de CSP.
• Autómata de entrada/salida
• Modelo de programación paralela
• TLA+ es otro lenguaje formal para modelar y verificar sistemas concurrentes.

Referencias

1. Roscoe, AW (1997). La teoría y la práctica de la concurrencia (PDF) . Prentice Hall . ISBN 978-0-13-674409-2.
2. Inmos (12 de mayo de 1995). Manual de referencia de occam 2.1 (PDF) . SGS-Thomson Microelectronics Ltd., Documento INMOS 72 occ 45 03.
3. Cox, Russ. "Bell Labs y CSP Threads" . Consultado el 15 de abril de 2010 .
4. "10 preguntas académicas e históricas" . Consultado el 15 de noviembre de 2021 .
5. "Preguntas frecuentes: ¿Por qué crear concurrencia a partir de las ideas de CSP?". El lenguaje de programación Go . Consultado el 15 de octubre de 2021 .
6. Hickey, Rich (28 de junio de 2013). «Canales core.async de Clojure» . Consultado el 15 de octubre de 2021 .
7. Hoare, CAR (1978). "Comunicación de procesos secuenciales". Comunicaciones de la ACM . 21 (8): 666–677. doi : 10.1145/359576.359585 . S2CID  849342.
8. Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Comunicación de procesos secuenciales: los primeros 25 años. LNCS . Vol. 3525. Springer. ISBN 9783540258131.
9. Barrett, G. (1995). "Verificación de modelos en la práctica: el procesador de canal virtual T9000". IEEE Transactions on Software Engineering . 21 (2): 69–78. doi :10.1109/32.345823.
10. Hall, A; Chapman, R. (2002). "Corrección por construcción: desarrollo de un sistema comercial seguro" (PDF) . IEEE Software . 19 (1): 18–25. CiteSeerX 10.1.1.16.1811 . doi :10.1109/52.976937. 
11. Creese, S. (2001). Inducción independiente de los datos: comprobación del modelo CSP de redes de tamaño arbitrario (D. Phil.). Universidad de Oxford . CiteSeerX 10.1.1.13.7185 . 
12. Hoare, CAR (1985). Comunicación de procesos secuenciales . Prentice Hall. ISBN 978-0-13-153289-2.
13. Clinger, William (junio de 1981). Fundamentos de la semántica de actores (tesis doctoral de matemáticas). MIT. hdl :1721.1/6935.
14. Brookes, Stephen; Hoare, CAR ; Roscoe, AW (1984). "Una teoría de los procesos secuenciales de comunicación". Revista de la ACM . 31 (3): 560–599. doi : 10.1145/828.833 . S2CID  488666.
15. Buth, B.; M. Kouvaras; J. Peleska; H. Shi (diciembre de 1997). "Análisis de interbloqueo para un sistema tolerante a fallos". Actas de la 6.ª Conferencia internacional sobre metodología algebraica y tecnología de software (AMAST'97) . págs. 60–75.
16. Buth, B.; J. Peleska; H. Shi (enero de 1999). "Combinación de métodos para el análisis de bloqueos activos de un sistema tolerante a fallos". Actas de la 7.ª Conferencia internacional sobre metodología algebraica y tecnología de software (AMAST'98) . págs. 124–139.
17. Lowe, G. (1996). "Rompiendo y reparando el protocolo de clave pública Needham–Schroeder usando FDR". Herramientas y algoritmos para la construcción y análisis de sistemas (TACAS) . Springer-Verlag. págs. 147–166.
18. Scattergood, JB (1998). La semántica y la implementación de CSP legible por máquina ( D.Phil. ). Laboratorio de Computación de la Universidad de Oxford .
19. Roscoe, AW (1994). "Verificación de modelos CSP". Una mente clásica: ensayos en honor a CAR Hoare . Prentice Hall.
20. "Introducción — Documentación de FDR 4.2.4". www.cs.ox.ac.uk .
21. Parashkevov, Atanas N.; Yantchev, Jay (1996). "ARC – una herramienta para el refinamiento eficiente y la verificación de equivalencia para CSP". Conferencia internacional IEEE sobre algoritmos y arquitecturas para procesamiento paralelo ICA3PP '96 . págs. 68–75. CiteSeerX 10.1.1.45.3212 . 
22. Leuschel, Michael; Fontaine, Marc (2008). "Probing the Depths of CSP-M: A new FDR-compliant Validation Tool" (PDF) . ICFEM 2008. Springer-Verlag. Archivado desde el original (PDF) el 19 de julio de 2011. Consultado el 26 de noviembre de 2008 .
23. Sun, Jun; Liu, Yang; Dong, Jin Song (2009). "PAT: Towards Flexible Verification under Fairness" (PDF) . Actas de la 20.ª Conferencia Internacional sobre Verificación Asistida por Computadora (CAV 2009) . Apuntes de clase en Ciencias de la Computación. Vol. 5643. Springer. Archivado desde el original (PDF) el 2011-06-11 . Consultado el 2009-06-16 .
24. Sun, Jun; Liu, Yang; Dong, Jin Song (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF) . Actas del Tercer Simposio Internacional sobre Aprovechamiento de Aplicaciones de Métodos Formales, Verificación y Validación (ISoLA 2008) . Comunicaciones en Ciencias de la Computación y la Información. Vol. 17. Springer. págs. 307–322. Archivado desde el original (PDF) el 2009-01-08 . Consultado el 2009-01-15 .
25. Sun, Jun; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "Integración de especificaciones y programas para la especificación y verificación de sistemas" (PDF) . IEEE Int. Conf. sobre aspectos teóricos de la ingeniería de software TASE '09 . Archivado desde el original (PDF) el 2011-06-11 . Consultado el 2009-04-13 .
26. Green, Mark; Abdallah, Ali (2002). "Análisis de rendimiento y ajuste del comportamiento para la optimización de sistemas de comunicación". Arquitecturas de procesos de comunicación 2002 .
27. Brooke, Phillip; Paige, Richard (2007). "Exploración y comprobación diferida de modelos CSP con CSPsim". Comunicación de arquitecturas de procesos 2007 .
28. ISO 8807, Especificación del lenguaje de ordenación temporal
29. Geraint Jones (1990). "Afilado como una navaja: un premio de la Reina para el laboratorio de computación". The Oxford Magazine (59, cuarta semana, período Trinity).
30. Len Shustek (marzo de 2009). "Una entrevista con CAR Hoare". Comunicaciones de la ACM . 52 (3): 38–41. doi :10.1145/1467247.1467261. S2CID  1868477.

Lectura adicional

• Hoare, CAR (2004) [1985]. Comunicación de procesos secuenciales. Prentice Hall International. ISBN 978-0-13-153271-7.
  • Este libro ha sido actualizado por Jim Davies en el Laboratorio de Computación de la Universidad de Oxford y la nueva edición está disponible para descargar como archivo PDF en el sitio web Using CSP.
• Roscoe, AW (1997). La teoría y la práctica de la concurrencia . Prentice Hall . ISBN 978-0-13-674409-2.
  • Algunos enlaces relacionados con este libro están disponibles aquí. El texto completo está disponible para descargar como archivo PS o PDF desde la lista de publicaciones académicas de Bill Roscoe.

Enlaces externos

• Una versión PDF del libro CSP de Hoare: se aplican restricciones de derechos de autor, consulte el texto de la página antes de descargarlo.
• La anotación de CSP (versión china), trabajo de traducción y anotación sin fines de lucro basado en el libro de Prentice-Hall (1985), la versión china de Chaochen Zhou (1988) y la versión en línea de Jim Davies (2015).
• WoTUG, un grupo de usuarios para sistemas de estilo CSP y Occam, contiene información sobre CSP y enlaces útiles.
• "Citas CSP" de CiteSeer