Comunicar procesos secuenciales.

Modelo formal en 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 se describió por primera vez en un artículo de 1978 de Tony Hoare , ^[7] pero desde entonces ha evolucionado sustancialmente. ^[8] 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í 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 pueden analizarse 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 la de 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 mediante el paso de mensajes sincrónico. A diferencia de versiones posteriores de CSP, a cada proceso se le asignaba un nombre explícito y el origen o destino de un mensaje se definía especificando el nombre del proceso de envío o recepción previsto. Por ejemplo, el proceso

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

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

[oeste::DESMONTAJE || X::COPIAR || este::ENSAMBLAJE]

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 hasta su forma algebraica de proceso moderna. El enfoque adoptado para convertir 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 fue presentada inicialmente en un artículo de 1984 por 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 todavía era el la tercera referencia informática más citada de todos los tiempos según Citeseer ^{[ cita necesaria ]} (aunque es una fuente poco confiable debido a la naturaleza de su muestreo). La teoría de la CSP ha sufrido algunos cambios menores desde la publicación del libro de Hoare. La mayoría de estos cambios fueron motivados por la llegada de herramientas automatizadas para el análisis y la verificación de procesos CSP. La teoría y práctica de la concurrencia ^[1] de Roscoe describe esta versión más nueva de CSP.

Aplicaciones

Una de las primeras e importantes aplicaciones de CSP fue su uso para la especificación y verificación de elementos del INMOS T9000 Transputer , un complejo procesador superescalar canalizado diseñado para soportar multiprocesamiento a gran escala. Se empleó CSP para verificar la corrección tanto de la canalización del procesador como del procesador de canal virtual, que gestionaba las comunicaciones fuera del chip para el procesador. ^[9]

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

Dado que CSP es adecuado para modelar y analizar sistemas que incorporan intercambios de mensajes complejos, también se ha aplicado a la verificación de protocolos de seguridad y comunicaciones. Un ejemplo destacado de este tipo de aplicación es el uso de Lowe's de CSP y el 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 comunicación de paso de mensajes . Sin embargo, la parte "Secuencial" del nombre CSP es ahora un nombre inapropiado, ya que el CSP moderno permite que los procesos componentes se definan como procesos secuenciales y como la composición paralela de procesos más primitivos. Las relaciones entre diferentes procesos y la forma en que cada proceso se comunica con su entorno se describen mediante varios operadores algebraicos de proceso . Utilizando este enfoque algebraico, se pueden construir fácilmente descripciones de procesos bastante complejos a partir de unos pocos elementos primitivos.

Primitivos

CSP proporciona dos clases de primitivas 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, encendido , apagado ), nombres compuestos (por ejemplo, válvula.abierta , válvula.cerrada ) o eventos de entrada/salida (por ejemplo, mouse?xy , pantalla!bitmap ).

Procesos primitivos

Los procesos primitivos representan comportamientos fundamentales: los ejemplos incluyen DETENER (el proceso que no comunica nada, también llamado interbloqueo ) y SALTAR (que representa una terminación exitosa).

Operadores algebraicos

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

Prefijo

El operador de prefijo combina un evento y un proceso para producir un nuevo proceso. Por ejemplo,

$${\displaystyle a\to P}$$

es el proceso que está dispuesto a comunicarse a con su entorno y, después de a , se comporta como el proceso P .

Elección determinista

El operador de elección determinista (o externo) permite que la evolución futura de un proceso se defina 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,

$${\displaystyle (a\to P)\Box (b\to Q)}$$

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 el entorno elija comunicar. Si a y b se comunicaran simultáneamente, la elección se resolvería de forma no determinista.

elección no determinista

El operador de elección no determinista (o interno) permite que la evolución futura de un proceso se defina 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,

$${\displaystyle (a\to P)\sqcap (b\to Q)}$$

puede comportarse como cualquiera o . Puede negarse a aceptar a o b y sólo está obligado a comunicar si el entorno ofrece tanto a como b . El no determinismo puede introducirse inadvertidamente en una elección nominalmente determinista si los acontecimientos iniciales de ambos lados de la elección son idénticos. Así por ejemplo, ${\displaystyle (a\to P)}$ ${\displaystyle (b\to Q)}$

$${\displaystyle (a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})}$$

es equivalente a

$${\displaystyle a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}}$$

Intercalado

El operador de entrelazado representa una actividad concurrente completamente independiente. El proceso

$${\displaystyle P\;|||\;Q}$$

se comporta como P y Q simultáneamente. Los acontecimientos de ambos procesos se entrelazan arbitrariamente en el tiempo.

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 interfaces solo puede ocurrir cuando todos los procesos componentes pueden participar en ese evento. Por ejemplo, el proceso

$${\displaystyle P\;|[\{a\}]|\;Q}$$

Requiere que P y Q sean capaces de realizar el evento a antes de que ese evento pueda ocurrir. Así, por ejemplo, el proceso

$${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$$

puede participar en el evento a y convertirse en el proceso

$${\displaystyle P\;|[\{a\}]|\;Q}$$

mientras

$${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$$

simplemente se estancará.

Ocultación

El operador oculto proporciona una forma de abstraer procesos al hacer que algunos eventos no sean observables. Un ejemplo trivial de ocultamiento es

$${\displaystyle (a\to P)\setminus \{a\}}$$

que, suponiendo que el evento a no aparece en P , simplemente se reduce 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 realizar dos eventos diferentes, “moneda” y “choc” que representan la inserción de un pago y la entrega de un chocolate respectivamente. Una máquina que exige el pago (sólo 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 podría optar 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 se pueden poner en paralelo para que puedan interactuar entre sí. El comportamiento del proceso compuesto depende de los eventos en los que los dos procesos componentes deben sincronizarse. De este modo,

$${\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 solo fuera requerida 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} }$$

Este es 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 .

Definicion 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 divergencia , así como varios operadores como paralelo alfabetizado, canalización y opciones indexadas. ${\displaystyle \mathbf {div} }$

Semántica formal

CSP ha sido imbuido de varias semánticas formales diferentes , que definen el significado de expresiones CSP sintácticamente correctas. La teoría de CSP incluye semántica denotacional , semántica algebraica y semántica operativa 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 . Los mapeos semánticos de expresiones de procesos a cada uno de estos tres modelos proporcionan la semántica denotacional para CSP. ^[1]

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

• ${\displaystyle \mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}}$ya que no realiza eventos ${\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 ningún evento, 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 , tiene prefijo cerrado) ${\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 rechazos, que son conjuntos de eventos que un proceso puede negarse a realizar. Un fallo es un par que consta de un seguimiento y un conjunto de rechazos X que identifica los eventos que un proceso puede rechazar una vez que ha ejecutado los seguimientos . 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/divergencia amplía 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 que 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 una serie de 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 CSP legible por máquina ideado por Bryan Scattergood , a veces denominado CSP _M. ^[18] El dialecto CSP _M de CSP posee una semántica operativa 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 a menudo se describe como un verificador de modelos , pero técnicamente es un verificador de refinamiento , en el sentido de que convierte dos expresiones de procesos 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 específico (rastros, fallas o fallas/divergencias). ^[19] FDR2 aplica varios algoritmos de compresión del espacio de estados a los LTS de proceso para reducir el tamaño del espacio de estados que debe explorarse durante una verificación de refinamiento. FDR2 ha sido sucedido por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, ejecución paralela y un verificador de tipos integrado. Lo publica la Universidad de Oxford, que también lanzó FDR2 en el período 2008-2012. ^[20]

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

El proyecto ProB , ^[22] organizado por el Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, se creó originalmente para respaldar el análisis de especificaciones construidas con el método B. Sin embargo, también incluye soporte para el análisis de los procesos CSP mediante la verificación de refinamiento y la verificación del modelo LTL . ProB también se puede utilizar para verificar las propiedades de las especificaciones CSP y B combinadas. Un animador ProBE CSP está integrado en FDR3.

El Process Analysis Toolkit (PAT) ^{[23] [24]} es una herramienta de análisis CSP desarrollada en la Escuela de Computación de la Universidad Nacional de Singapur . PAT puede realizar comprobaciones de refinamiento, comprobaciones de modelos LTL y simulación de procesos CSP y CSP cronometrado. El lenguaje de proceso PAT amplía CSP con soporte para variables compartidas mutables, paso de mensajes asincrónicos 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 de procedimiento (por ejemplo, un evento en PAT puede ser un programa secuencial o incluso una llamada a una biblioteca C# externa) para una mayor expresividad. Las variables compartidas mutables y los canales asincrónicos proporcionan un azúcar sintáctico conveniente para patrones de modelado de procesos conocidos utilizados 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 el CSP _M estándar son el uso de punto y coma para terminar expresiones de proceso, la inclusión de azúcar sintáctico para variables y asignaciones, y el uso de sintaxis ligeramente diferente para elección interna y composición paralela.

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

CSPsim ^[27] es un simulador vago. No verifica el modelo 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 sólo como expresiones 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 comprobaciones de refinamiento, puede realizar comprobaciones de interbloqueo y de bloqueo activo.

Formalismos relacionados

Varios otros lenguajes de especificación y formalismos se han derivado o inspirado en el CSP clásico sin tiempo, entre ellos:

• CSP cronometrado ^{[ enlace muerto permanente ]} , que incorpora información de temporización para razonar sobre sistemas en tiempo real
• Teoría del proceso receptivo, una especialización de CSP que asume una operación de envío asincrónica (es decir, sin bloqueo )
• CSPP
• HCSP
• 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 la Programación
• CML Archivado el 19 de febrero de 2020 en Wayback Machine (COMPASS Modeling Language), 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 ocupa de procesos concurrentes que intercambian mensajes, el modelo de actor es muy similar al CSP. Sin embargo, los dos modelos toman decisiones fundamentalmente diferentes con respecto a las primitivas que proporcionan:

• Los procesos de CSP son anónimos, mientras que los actores tienen identidades.
• 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 efectivamente tienen 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 involucrados 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 los sistemas de actores es fundamentalmente asíncrono, es decir, la transmisión y 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 se pueden usar para construir comunicaciones almacenadas en búfer que se comportan como sistemas de mensajería asíncronos, mientras que los sistemas asíncronos se pueden usar para construir comunicaciones de estilo encuentro mediante el uso de un mensaje/ Protocolo de reconocimiento para sincronizar remitentes y receptores.

Tenga en cuenta que las propiedades antes mencionadas no necesariamente se refieren al artículo CSP original de Hoare, sino más bien a la encarnación moderna de la idea como se ve en implementaciones como Go y Clojure's core.async. En el artículo original, los canales no eran una parte central de la especificación y los procesos de remitente y receptor en realidad se identifican entre sí por su nombre.

Otorgar

En 1990, “ Se otorgó el Premio de la Reina al Logro Tecnológico... 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 ' transputador ', un microprocesador con muchas de las piezas que normalmente se necesitarían además integradas en el mismo componente único ”. ^[29] Según Tony Hoare, ^[30] “El INMOS Transputer 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 CSP estaban maduras para la explotación industrial y creó la base del lenguaje para programar Transputers, que se llamó Occam . … La empresa estimó que les permitió entregar el hardware un año antes de lo que hubiera sucedido de otro modo. Solicitaron y ganaron el premio Queen por logros tecnológicos, en conjunto con el Laboratorio de Computación de la Universidad de Oxford”.

Ver también

• Teoría de las huellas , teoría general de las huellas.
• Traza monoide y monoide histórico
• Lenguaje de programación sencillo
• lenguaje de programación xc
• VerilogCSP es un conjunto de macros agregadas a Verilog HDL para admitir 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 funciones de CSP como el encuentro.
• DirectShow es el marco de video dentro de DirectX , utiliza los conceptos de CSP para implementar los filtros de audio y video.
• OpenComRTOS es un RTOS distribuido centrado en la red desarrollado formalmente y 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 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. "Subprocesos Bell Labs y CSP" . Consultado el 15 de abril de 2010 .
4. "Diez preguntas académicas e históricas" . Consultado el 15 de noviembre de 2021 .
5. "Preguntas frecuentes: ¿Por qué generar simultaneidad sobre las ideas de CSP?". El lenguaje de programación Go . Consultado el 15 de octubre de 2021 .
6. Hickey, rico (28 de junio de 2013). "Canales Clojure core.async" . Consultado el 15 de octubre de 2021 .
7. Hoare, COCHE (1978). "Comunicar procesos secuenciales". Comunicaciones de la ACM . 21 (8): 666–677. doi : 10.1145/359576.359585 . S2CID  849342.
8. Abdallah, Ali E.; Jones, acantilado B.; Lijadoras, Jeff W. (2005). Comunicación de procesos secuenciales: los primeros 25 años. LNCS . vol. 3525. Saltador. ISBN 9783540258131.
9. Barrett, G. (1995). "Comprobación de modelos en la práctica: el procesador de canal virtual T9000". Transacciones IEEE sobre ingeniería de software . 21 (2): 69–78. doi : 10.1109/32.345823.
10. Salón, A; Chapman, R. (2002). "Corrección por construcción: desarrollo de un sistema comercial seguro" (PDF) . Software IEEE . 19 (1): 18–25. CiteSeerX 10.1.1.16.1811 . doi : 10.1109/52.976937. 
11. Creese, S. (2001). Inducción independiente de datos: verificación del modelo CSP de redes de tamaño arbitrario (D. Phil.). Universidad de Oxford . CiteSeerX 10.1.1.13.7185 . 
12. Hoare, COCHE (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 en Matemáticas). MIT. hdl :1721.1/6935.
14. Brookes, Esteban; Hoare, COCHE ; Roscoe, AW (1984). "Una teoría de la comunicación de procesos secuenciales". Revista de la ACM . 31 (3): 560–599. doi : 10.1145/828.833 . S2CID  488666.
15. Pero, B.; M. Kouvaras; J. Peleska; H. Shi (diciembre de 1997). "Análisis de punto muerto para un sistema tolerante a fallos". Actas de la VI Conferencia Internacional sobre Metodología Algebraica y Tecnología de Software (AMAST'97) . págs. 60–75.
16. Pero, B.; J. Peleska; H. Shi (enero de 1999). "Combinación de métodos para el análisis livelock de un sistema tolerante a fallos". Actas de la Séptima Conferencia Internacional sobre Metodología Algebraica y Tecnología de Software (AMAST'98) . págs. 124-139.
17. Lowe, G. (1996). "Romper y arreglar el protocolo de clave pública Needham-Schroeder utilizando 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). "CSP de verificación de modelos". 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 de CSP". IEEE Internacional. Conf. 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). "Sondeando las profundidades de CSP-M: una nueva herramienta de validación compatible con FDR" (PDF) . ICFEM 2008 . Springer-Verlag. Archivado desde el original (PDF) el 19 de julio de 2011 . Consultado el 26 de noviembre de 2008 .
23. Sol, junio; Liu, Yang; Dong, Jin Song (2009). "PAT: Hacia una verificación flexible y justa" (PDF) . Actas de la XX Conferencia Internacional sobre Verificación Asistida por Computadora (CAV 2009) . Apuntes de conferencias sobre informática. vol. 5643. Saltador. Archivado desde el original (PDF) el 11 de junio de 2011 . Consultado el 16 de junio de 2009 .
24. Sol, junio; Liu, Yang; Dong, Jin Song (2008). "Revisión del CSP de verificación de modelos: presentación de un conjunto de herramientas de análisis de procesos" (PDF) . Actas del Tercer Simposio Internacional sobre Aprovechamiento de Aplicaciones de Métodos Formales, Verificación y Validación (ISoLA 2008) . Comunicaciones en Informática y Ciencias de la Información. vol. 17. Saltador. págs. 307–322. Archivado desde el original (PDF) el 8 de enero de 2009 . Consultado el 15 de enero de 2009 .
25. Sol, junio; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "Integración de especificaciones y programas para la especificación y verificación del sistema" (PDF) . IEEE Internacional. Conf. sobre Aspectos Teóricos de la Ingeniería de Software TASE '09 . Archivado desde el original (PDF) el 11 de junio de 2011 . Consultado el 13 de abril de 2009 .
26. Verde, marca; Abdallah, Ali (2002). "Análisis de rendimiento y ajuste de comportamiento para la optimización de sistemas de comunicación". Comunicación de arquitecturas de procesos 2002 .
27. Brooke, Phillip; Paige, Richard (2007). "Exploración diferida y verificación de modelos CSP con CSPsim". Comunicación de arquitecturas de procesos 2007 .
28. ISO 8807, Idioma de especificación de pedidos temporales
29. Geraint Jones (1990). "Afilado como una navaja: premio de la reina para el laboratorio de informática". 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.

Otras lecturas

• Hoare, CAR (2004) [1985]. Comunicación de procesos secuenciales. Prentice Hall Internacional. ISBN 978-0-13-153271-7.
  • Este libro ha sido actualizado por Jim Davies del 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 de Uso de CSP.
• Roscoe, AW (1997). La teoría y 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.
• The Annotation of 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 CSP y sistemas de estilo occam, contiene información sobre CSP y enlaces útiles.
• "Citas de CSP" de CiteSeer