scd-t1-intro.pdf

Sistemas Concurrentes y Distribuidos: Tema 1. Introducción. Carlos Ureña / Jose M. Mantas / Pedro Villar / Manuel Noguera Curso 2024-25 (archivo generado el 18 de septiembre de 2024) Grado en Ingeniería Informática Dpt. Lenguajes y Sistemas Informáticos ETSI Informática y de Telecomunicación Unive...

Sistemas Concurrentes y Distribuidos: Tema 1. Introducción. Carlos Ureña / Jose M. Mantas / Pedro Villar / Manuel Noguera Curso 2024-25 (archivo generado el 18 de septiembre de 2024) Grado en Ingeniería Informática Dpt. Lenguajes y Sistemas Informáticos ETSI Informática y de Telecomunicación Universidad de Granada  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Índice. 1. Conceptos básicos y motivación 2. Modelo abstracto y consideraciones sobre el hardware 3. Exclusión mutua y sincronización 4. Propiedades de los sistemas concurrentes 5. Verificación de programas concurrentes  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 1. Conceptos básicos y motivación. 1.1. Conceptos básicos relacionados con la concurrencia 1.2. Motivación de la Programación concurrente  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 1. Conceptos básicos y motivación Subsección 1.1. Conceptos básicos relacionados con la concurrencia. Concurrencia: programa y programación concurrentes I Programa secuencial: Declaraciones de datos + Conjunto de instrucciones sobre dichos datos que se deben ejecutar en secuencia. I Programa concurrente: Conjunto de programas secuenciales ordinarios que se pueden ejecutar lógicamente en paralelo. I Proceso: Ejecución de un programa secuencial. I Concurrencia: Describe el potencial para ejecución paralela, es decir, el solapamiento real o virtual de varias actividades en el tiempo. I Programación Concurrente (PC): Conjunto de notaciones y técnicas de programación usadas para expresar paralelismo potencial y resolver problemas de sincronización y comunicación. I La PC es independiente de la implementación del paralelismo. Es una abstracción Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 5 de 91. Programación paralela, distribuida y de tiempo real I Programación paralela: Su principal objetivo es acelerar la resolución de problemas concretos mediante el aprovechamiento de la capacidad de procesamiento en paralelo del hardware disponible. I Programación distribuida: Su principal objetivo es hacer que varios componentes software localizados en diferentes ordenadores (o, en general, sin memoria compartida) trabajen colaborativamente. I Programación de tiempo real: Se centra en la programación de sistemas que están funcionando continuamente, recibiendo entradas y enviando salidas a/desde componentes hardware (sistemas reactivos), en los que se trabaja con restricciones muy estrictas en cuanto a la respuesta temporal (sistemas de tiempo real). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 6 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 1. Conceptos básicos y motivación Subsección 1.2. Motivación de la Programación concurrente. Beneficios de la Programación concurrente La programación concurrente es más compleja que la programación secuencial, entonces nos preguntamos: ¿ Por qué es necesario conocer la Programación Concurrente ? Básicamente hay dos motivos para el desarrollo de la programación concurrente: I Mejora de la eficiencia I Mejoras en la calidad Veremos ambos aspectos. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 8 de 91. Beneficios P.C.: Mejora de la eficiencia. La PC permite aprovechar mejor los recursos hardware existentes. I En sistemas con un solo procesador: I Al tener varias tareas, cuando la tarea que tiene el control del procesador necesita realizar una E/S cede el control a otra, evitando la espera ociosa del procesador. I También permite que varios usuarios usen el sistema de forma interactiva (actuales sistemas operativos multisusuario). I En sistemas con varios procesadores: I Es posible repartir las tareas entre los procesadores, reduciendo el tiempo de ejecución. I Fundamental para acelerar complejos cómputos numéricos. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 9 de 91. Beneficios P.C.: Mejora de la calidad Muchos programas se entienden mejor en términos de varios procesos secuenciales ejecutándose concurrentemente que como un único programa secuencial. Ejemplos: I Servidor web para reserva de vuelos: Es más natural, considerar cada petición de usuario como un proceso e implementar políticas para evitar situaciones conflictivas (permitir superar el límite de reservas en un vuelo). I Simulador del comportamiento de una gasolinera: Es más sencillo considerar los surtidores, clientes, vehículos y empleados como procesos que cambian de estado al participar en diversas actividades comunes, que considerarlos como entidades dentro de un único programa secuencial. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 10 de 91. Programas de cálculo intensivo En la actualidad hay múltiples aplicaciones de cálculo intensivo que se benefician de la programación concurrente y distribuida. I Cálculo intensivo en múltiples CPUs: en la actualidad, los ordenadores incorporan múltiples CPUs. Un programa secuencial puede usar únicamente una de ellas, mientras que un programa concurrente puede usar varias a la vez de forma coordinada. I Cálculo intensivo en GPUs: uso de programación concurrente para cálculos intensivos en GPUs aprovechando su hardware que incorpora cientos o miles de unidades de cálculo flotante. I Sistemas distribuidos de cálculo: permiten cálculos intensivos en varios ordenadores conectados a un red, con paso de mensajes entre ellos. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 11 de 91. Aplicaciones del cálculo intensivo Como consecuencia, la programación concurrente se ha convertido en una herramienta esencial en diversas áreas que requieren cálculo intensivo, podemos citar algunas: I Videojuegos, realidad virtual y aumentada: la PC se usa para visualización, simulación física e I.A. de personajes. I Inteligencia artificial: entrenamiento de redes neuronales o en general aprendizaje de sistemas de IA. También su uso una vez entrenadas. I Animación y rendering: generación off-line de animaciones y efectos especiales en películas. I Simulación de sistemas físicos: predicción meteorológica, cálculo de estructuras de edificios u objetos, simulación de viento o fluidos, etc... I Cálculo de estructuras moleculares: simulación computacional del comportamiento y estructura de moléculas y proteínas. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 12 de 91. Programación Web o en Internet La programación distribuida constituye el modelo subyacente a la programación de aplicaciones Web, en las cuales distintos procesos (probablemente en distintos ordenadores) se comunican mediante mecanismos de paso de mensajes. Ejemplos: I Comunicación distribuida (típicamente siguiendo el modelo cliente-servidor, que veremos más adelante) mediante distintas modalidades de paso de mensajes. I Programación asíncrona en clientes Web: permite simultanear el procesamiento, las transferencias de datos y la interacción con el usuario. I Uso concurrente de varias CPUs en un cliente Web, con coordinación y comunicación mediante paso de mensajes. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 13 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 2. Modelo abstracto y consideraciones sobre el hardware. 2.1. Consideraciones sobre el hardware 2.2. Modelo abstracto de un proceso secuencial 2.3. Modelo abstracto de ejecución concurrente  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 2. Modelo abstracto y consideraciones sobre el hardware Subsección 2.1. Consideraciones sobre el hardware. Modelos de arquitecturas para programación concurrente Mecanismos de implementación de la concurrencia I Dependen fuertemente de la arquitectura. I Consideran una máquina virtual que representa un sistema (multiprocesador o sistema distribuido), proporcionando una base homogénea para la ejecución de procesos concurrentes. I El tipo de paralelismo afecta a la eficiencia, pero no a la corrección. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 16 de 91. Concurrencia en sistemas monoprocesador Ordenador CPU Memoria I Multiprogramación: El sistema operativo gestiona cómo múltiples procesos se reparten los ciclos de la (única) CPU. I Mejor aprovechamiento CPU. I Servicio interactivo a varios usuarios. I Permite usar soluciones de diseño concurrentes. I Se hace sincronización y comunicación mediante variables compartidas en la memoria. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 17 de 91. Concurrencia en multiprocesadores de memoria compartida Ordenador CPU1 CPU2 ··· CPUn Memoria I Los procesadores pueden compartir o no físicamente la misma memoria, pero siempre comparten un espacio de direcciones compartido. I La interacción entre los procesos se puede implementar mediante variables alojadas en direccciones del espacio compartido (variables compartidas). I Ejemplo: PCs con procesadores multicore. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 18 de 91. Concurrencia en sistemas distribuidos Red de interconexión Ord.1 Ord.2 Ord.3 Ord.N CPU CPU CPU CPU ······ Memoria Memoria Memoria Memoria I No existe una memoria común: cada procesador tiene su espacio de direcciones privado. I Los procesadores interaccionan transfiriéndose datos a través de una red de interconexión (paso de mensajes). I Programación distribuida: además de la concurrencia, trata con otros problemas como el tratamiento de los fallos, transparencia, heterogeneidad, etc. I Ejemplos: Clusters de ordenadores, internet, intranet. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 19 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 2. Modelo abstracto y consideraciones sobre el hardware Subsección 2.2. Modelo abstracto de un proceso secuencial. Programa secuencial. Un programa secuencial es un texto fuente que incluye decla- raciones de variables y sentencias, las cuales se ejecutarán de forma secuencial. De forma secuencial quiere decir ordenada en el tiempo: hasta que no acaba la ejecución de una sentencia, no comienza la si- guiente.   Process EjemploSec ; var x : integer := 0 ; A la derecha, vemos un ejem- y : integer := 2 ; plo de un programa secuencial begin while x < 2 do begin en pseudo-código (una nota- x := x+1 ; ción inspirada en los lenguajes y := 2*y+x+1 ; end Algol y Pascal): print(x,y); end   Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 21 de 91. Sentencias, estados y procesos sencuenciales. Una sentencia es un trozo del texto de un programa el cual, al ejecutarse, modifica el valor de una o de varias variables del pro- grama, para ello realiza uno o varios accesos de escritura a las mismas. Un estado de un programa es el conjunto de valores de las va- riables del programa en un instante durante su ejecución. Un proceso secuencial es una ejecución (en un tiempo finito) de un programa secuencial. Durante dicha ejecución, se ejecutan las sentencias del progra- ma, que cambian las variables desde un estado inicial hasta un estado final. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 22 de 91. Accesos a variables en una sentencia Un acceso a una variable es una operación realizada por el proce- sador por la cual lee o escribe dicha variable durante la ejecución de un programa. I Consideramos únicamente accesos a variables de tipos primitivos: lógicos, enteros, carácter o flotantes (un acceso a una variables compuesta es una secuencia de accesos a variables primitivas). I Cuando se ejecuta una sentencia, se producen uno varios de estos accesos, los cuales se realizan también de forma secuencial, es decir: hasta que no acaba uno no puede comenzar el siguiente. I La sentencias más simples posibles producen un único acceso de escritura, por ejemplo, x:=34. I Las asignaciones con expresiones más complejas, y otros tipos de sentencias, producen típicamente más de un acceso. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 23 de 91. Variables accedidas por una sentencia El conjunto V (S) de variables accedidas por una sentencia S es el conjunto de variables que se leen o escriben durante una ejecución de S. Ejemplos tomados del programa: I La sentencia x:=x+1 accede a la variable x (la lee y la escribe). El conjunto es: V (x:=x+1) = {x} I La sentencia y:=2*y+x+1 accede a las variables x e y (lee ambas y escribe y). El conjunto es: V (y:=2*y+x+1) = {x, y} I La sentencia print(x,y) accede a las variables x e y (las lee). V (print(x,y)) = {x, y} Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 24 de 91. Traza y ejemplo (1/2) La historia o traza de una ejecución de un proceso secuencial es la secuencia de estados por los que pasa el proceso durante dicha ejecución. A modo de ejemplo, para analizar su traza, consideramos el programa secuencial que hemos visto. Se parte de un estado inicial (a la izquierda), se ejecuta la sentencia while (en el centro) y se llega a un estado final (a la derecha). while x < 2 do begin x≡0 x := x+1 ; x≡2 y≡2 y := 2*y+x+1 ; y ≡ 15 end I Las sentencias tienen fondo gris y los estados fondo rojo. I En este caso vemos una sentencia while, la cual a su vez está compuesta de otras sentencias. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 25 de 91. Traza y ejemplo. (2/2) La ejecución de la sentencia while en realidad se descompone en la doble ejecución de la sentencia bloque (entre begin y end), por tanto, se produce un estado intermedio (en el centro). begin begin x≡0 x := x+1 ; x≡1 x := x+1 ; x≡2 y≡2 y := 2*y+x+1 ; y≡6 y := 2*y+x+1 ; y ≡ 15 end end Cada ejecución del bloque se descompone a su vez en dos sentencias de asignación, así que la secuencia de estados detallada a nivel de asignaciones sería esta: x≡0 x≡1 x≡1 x≡2 x≡2 x:= x+1; y:= 2*y+x+1; x:= x+1; y:= 2*y+x+1; y≡2 y≡2 y≡6 y≡6 y ≡ 15 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 26 de 91. Tradución de expresiones aritméticas. Registros. En el pseudo-código se pueden usar expresiones aritméticas enteras, flotantes o lógicas, como, por ejemplo, las expresiones enteras x+1 o 2*y+x+1 que aparecen en el programa de ejemplo. I Para poder evaluarlas, una CPU necesita que los operandos de los operadores aritmético-lógicos (+,-,*,and, or, etc...) se guarden en los llamados registros del procesador. I A efectos de analizar el comportamiento, suponemos que cada proceso secuencial cuenta con una o varias variables propias (implícitamente declaradas), llamadas también registros, que se usan para evaluar las expresiones. Las llamamos r0, r1, r2, etc.... I Por cada referencia a una variable en una expresión, se debe hacer una lectura de la variable y una escritura en un registro. I Los valores de los registros forman parte del estado del proceso secuencial. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 27 de 91. Ejemplos de sentencias y sus accesos a memoria. A modo de ejemplo, la sentencia de asignación x:=x+1 se traduce al compilar en la sentencia compuesta r0:=x ; x:=r0+1, es decir, se hace: 1. r0:=x lectura de x y escritura en el registro r0 2. x:=r0+1 lectura de r0, cálculo de r0+1 y escritura sobre x. A modo de ejemplo, partiendo del estado (x==0,y==2), se produce esta traza: x≡0 x≡0 x≡1 y≡2 r0:= x; y≡2 x:= r0+1; y≡2 r0 ≡ - r0 ≡ 0 r0 ≡ 0 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 28 de 91. Traza de asignaciones usando dos registros En otras expresiones más complejas, se necesitan más de un registro y más de una lectura, por ejemplo, para y:=2*y+x+1 se necesitan dos registros (pues hay dos referencias a variables en la expresión a la derecha de :=), los pasos son: 1. r0:=y acceso de lectura a y, y escritura en el registro r0. 2. r1:=x acceso de lectura a x, y escritura en el registro r1. 3. y:=2*r0+r1+1 evaluación de la expresión (lectura de r0 y r1), seguida de acceso de escritura en y. Partiendo del estado (x==1,y==2) se obtiene esta traza: x ≡ 1 x ≡ 1 x ≡ 1 x ≡ 2 y ≡ 2 y ≡ 2 y ≡ 2 y ≡ 6 r0:= y; r1:= x; y:= 2*r0+r1+1 ; r0 ≡ - r0 ≡ 2 r0 ≡ 2 r0 ≡ 2 r1 ≡ - r1 ≡ - r1 ≡ 1 r1 ≡ 1 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 29 de 91. Sentencias compuestas y traza La traza puede escribirse en forma de tabla, en la primera fila aparece el estado inicial, después, en cada fila aparece una sentencia y el estado después de ejecutarse. A nivel de asignaciones, sería así: Sentencia Estado ejecutada x y 0 2 x := x+1 1 2 y := 2*y+x+1 1 6 x := x+1 2 6 y := 2*y+x+1 2 15 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 30 de 91. Traza detallada con un acceso por fila (2/2) Vemos la traza detallada, incluyendo las operaciones con registros: Sentencia Estado ejecutada r0 r1 x y - - 0 2 r0 := x 0 - 0 2 x := r0+1 0 - 1 2 r0 := y 2 - 1 2 r1 := x 2 1 1 2 y := 2*r0+r1+1 2 1 1 6 r0 := x 1 - 1 6 x := r0+1 1 - 2 6 r0 := y 6 - 2 6 r1 := x 6 2 2 6 y := 2*r0+r1+1 6 2 2 15 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 31 de 91. El proceso secuencial como secuencia de accesos En resumen: La ejecución de un proceso secuencial se puede modelar como una secuencia finita y ordenada de accesos a las variables (de tipos simples) declaradas explícitamente en el correspondiente programa, a partir del estado inicial. I Suponemos que la secuencia es finita porque el proceso nunca entra en en un bucle infinito (siempre se llega a un estado final). I Este modelo de un proceso secuencial es el que usaremos para analizar el comportamiento de programas concurrentes en memoria compartida (en la siguiente subsección). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 32 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 2. Modelo abstracto y consideraciones sobre el hardware Subsección 2.3. Modelo abstracto de ejecución concurrente. Programa concurrente. Un programa concurrente es un texto fuente que incluye declara- ciones de variables (algunas de ellas compartidas) y sentencias, de forma que dichas sentencias determinan cómo dos o más pro- cesos secuenciales se pueden ejecutar concurrentemente. Aquí concurrentemente quiere decir que la ejecución de cada sentencia de cada proceso secuencial puede solaparse en el tiem- po con las ejecución de sentencias del resto de procesos secuen- ciales. I Las variables compartidas son variables accesibles (para leer o escribir) por cualquiera de los procesos secuenciales que se ejecuten. I Además de las variables compartidas, cada proceso puede tener sus propias variables locales y sus propios registros (en ambos casos son no accesibles por otros procesos). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 34 de 91. Ejemplo de programa concurrente. A modo de ejemplo, vemos aquí un programa concurrente (usando una de las posibles formas de escribirlo)   { Variables compartidas } I Hay dos procesos secuenciales: var x : integer := 0 ; NomUno y NomDos. y : integer := 2 ; I Ambos acceden a las variables { Procesos secuenciales } compartidas (x e y). process NomUno ; var a : integer := 1 ; I Antes de ejecutar los procesos, begin x := x+1 ; se inicializan las variables com- end partidas. process NomDos ; var b : integer := 2 ; I A partir de ahí, ambos procesos begin se ejecutan concurrentemente. y := y+x+1 ; I El programa acaba cuando han end  acabado los dos procesos. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 35 de 91. Variables locales y registros En un programa concurrente: I Cada proceso secuencial puede incluir declaraciones de sus propias variables locales: son variables que únicamente pueden ser accedidas por el proceso secuencial donde están declaradas. En el ejemplo: I La variable a es local al proceso NomUno I La variable b es local al proceso NomDos I Dos variables locales de dos procesos secuenciales distintos podrían tener el mismo nombre (siguen siendo dos variables distintas). I Cada proceso secuencial usa sus propios registros para poder ejecutar las sentencias aritmético-lógicas, (esos registros son equivalentes a variables locales, en el sentido de que únicamente son accesibles por su proceso y no los otros). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 36 de 91. Notación abreviada para ejecución secuencial o concurrente. Si S A y SB son dos sentencias, podemos hablar de la ejecución secuencial o la ejecución concurrente de ambas. Por simplicidad a veces usaremos una notación abreviada: I Usaremos S A ;SB para denotar la sentencia compuesta cuya ejecución consiste en ejecutar S A completa, y después, cuando haya acabado, ejecutar SB completa (es decir secuencialmente). I Usaremos S A kSB para denotar la sentencia compuesta cuya ejecución consiste en ejecutar S A y SB de forma simultánea (es decir: concurrentemente). Esta sentencia acaba cuando hayan acabado tanto S A como SB. I Ambas construcciones pueden extenderse a más de dos sentencias, por ejemplo S A ;SB ;SC o bien S A kSB kSC I La sentencia S A kSB es equivalente a SB kS A , pero S A ;SB no es igual a SB ;S A. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 37 de 91. Accesos a variables compartidas: consistencia secuencial Es necesario suponer que siempre se cumple esta propiedad: Propiedad de Consistencia Secuencial Estricta: I La totalidad de los accesos a las variables realizados por to- dos los procesos (desde el inicio hasta el fin) ocurren en un orden determinado, sin solaparse: hasta que no ha acabado un acceso, no comienza el siguiente (incluso si son dos ac- cesos a variables distintas). Ese orden puede ser distinto en cada ejecución. I En ese orden de todos los accesos, los accesos realizados por un proceso secuencial P aparecen en el mismo orden en el que P los realiza. I El valor leído en una variable es siempre el último valor es- crito en ella, o el valor inicial si ningún proceso ha escrito aun en la variable. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 38 de 91. Estados de un programa concurrente Puesto que suponemos que se cumple la propiedad anterior, podemos hablar de los estados de un programa concurrente: Un estado de un programa concurrente es el conjunto de valores de las variables (compartidas y locales de cada proceso secuen- cial) en un instante durante su ejecución. Al igual que en un proceso secuencial, hay: I Un estado inicial y otro final. I Un estado distinto entre cada dos accesos consecutivos (según el orden conjunto), ahora esos dos accesos pueden ser del mismo proceso o de dos procesos distintos. Por tanto, cabe hablar también de la traza de un programa concurrente. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 39 de 91. Ejecución de sentencias de forma concurrente Durante la ejecución de una sentencia S1 en un programa concurrente: I La sentencia producirá una secuencia ordenada de accesos a las variables compartidas I Es posible que otra sentencia S2 de otro proceso también acceda a alguna de esas mismas variables compartidas (si V (S1 ) tiene alguna variable compartida en común con V (S2 )). I Si eso ocurre, el resultado de la ejecución de las sentencias S1 y S2 puede depender no solo de los valores de las variables y de las sentencias, sino también del orden en el que se mezclan los accesos. Esta es una característica importante de la programación concurrente que debe ser tenida muy en cuenta para el diseño de programas concurrentes. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 40 de 91. Ejemplo de ejecución concurrente de sentencias Supongamos que dos procesos secuenciales comparten una variable entera x que vale 0 en un estado, y después de ese estado ambos procesos ejecutan la sentencia x:=x+1 a la vez: I Cada proceso usa su propio registro r0 I Cada proceso ejecuta estas dos dos sentencias en secuencia: 1. lectura de la variable: r0:=x, 2. cálculo del nuevo valor y escritura: x:=r0+1. I Cuando hayan acabado ambas sentencias, el valor final de x dependerá del ordenamiento de los accesos. I Ese orden puede ser cualquiera y por tanto hay indeterminación: no hay un único estado posterior, sino que puede haber varios (dependiendo del orden) Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 41 de 91. Sentencias atómicas y no atómicas (1/2) Para simplificar el análisis y diseño de programas concurrentes, se introduce la noción de sentencia atómica: Sentencia atómica Una sentencia S de un proceso en un programa concurrente es atómica si y solo si siempre que se ejecuta (por un proceso se- cuencial P) no produce estados intermedios en V (S) que sean accesibles para otros procesos secuenciales distintos de P. I Consideramos estado intermedio a un estado que no es ni el inicial ni el final, y que está entre dos accesos a variables compartidas producidos por S. I Un estado es accesible para otros procesos si contiene va- lores de variables compartidas que puedan ser escritos o leídos por otros procesos distintos de P. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 42 de 91. Sentencias atómicas y no atómicas (2/2) Durante la ejecución de una sentencia atómica S por parte de un proceso P: I Los procesos distintos de P no pueden leer valores intermedios en las variables de V (S), ni pueden modificar, mediante escrituras, esos valores intermedios. I Es decir, los procesos distintos de P solo pueden acceder al estado previo o al estado posterior: los posibles cambios de valores de las variables en V (S) ocurren aparentemente de una vez para el resto de procesos. I Según la definición, es atómica cualquier sentencia que únicamente hace un acceso a una variable compartida (ya que nunca produce estados intermedios). I Existen sentencias atómicas con estados intermedios que no son accesibles por otros procesos (lo vemos más adelante). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 43 de 91. Ejemplos de sentencias atómicas (1/3). Hay diversos tipos de sentencias atómicas, a modo de ejemplo (sin ser exhaustivos), vemos estos: I Sentencias que no producen estados intermedios y únicamente realizan un acceso a una variable compartida, por ejemplo: I Escribir un valor en una variable compartida: x:=34. I Leer el valor de una variable compartida y escribirlo en un registro: r0:=x. I Leer el valor de un registro y escribirlo en una variable compartida: x:=r0. Estas sentencias típicamente se traducen en una única instrucción de código máquina, aunque ese detalle es irrelevante para la concurrencia: nos basta saber que son atómicas siempre y nos abstraemos de los detalles del hardware y el repertorio de instrucciones máquina. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 44 de 91. Ejemplos de sentencias atómicas (2/3). También son atómicas este otro tipo de sentencias (en adelante, suponemos que x e y son variables compartidas y a y b son variables locales): I Sentencias con múltiples accesos a variables, pero como mucho uno de ellos a una variable compartida. Ejemplos: I Realizar varios operaciones con registros y/o variables locales, y además escribir una vez en una variable compartida, por ejemplo: x:=2*r0+r1 o bien x:=a+b. I Igual, pero con una única lectura en una variable compartida, por ejemplo a:=2*b+x+1, o bien r0:=r1+x. I Operaciones con uno o varios accesos, pero ninguno de ellos a variables compartidas, por ejemplo: r0:=r0+1, o bien a:=2*b+a+1. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 45 de 91. Ejemplos de sentencias atómicas (3/3). Una sentencia compuesta puede ser atómica, si cumple la definición, aunque realize muchas operaciones. Por ejemplo, estas dos sentencias bloque son atómicas (siendo a y b locales y x e y compartidas):    begin begin a := 2*a*a + 3*b + 4 ; a := 2*a*a + 3*b + 4 ; b := b+1 ; b := b+1 ; x := 2*(a+b) ; { escribe x } a := 2*x*(a+b); { lee x } b := b-1 ; b := b-1 ; end end    I La sentencia de la izquierda accede a sus variables locales y produce una única escritura en una variable compartida. El resto de procesos únicamente podrán detectar un único cambio atómico del valor de la variable x. I La sentencia de la derecha realiza una única lectura de una variable compartida (y cambia el estado de sus variables locales). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 46 de 91. Ejemplos de sentencias no atómicas Muchas sentencias son no atómicas (producen estados intermedios que sí pueden ser accedidos por otras hebras), esencialmente debido a que esas sentencias hacen más de una operación de lectura y/o escritura en variables compartidas. Por ejemplo: I La sentencia x:=x+1, produce un estado intermedio, posterior a la lectura de x pero previo a la escritura en x. I La sentencia x:=x+y, produce dos estados intermedios (cada uno inmediatamente posterior a una de las dos lecturas). I Si una sentencia tiene dos o más lecturas de variables compartidas, es no atómica, aunque no tenga escrituras. Por ejemplo, la sentencia a:=x+y, produce un estado intermedio accesible en las variables compartidas, que ocurre entre la lectura de x y la de y. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 47 de 91. Ejemplo de solapamiento de instrucciones atómicas (1/2) Supongamos que dos procesos secuenciales PA y PB ejecutan concurrentemente las sentencias atómicas S A (x:=a+1) y SB (b:=x+1) partiendo de un estado en el que x (compartida), a (local de PA ) y b (local de PB ) valen todas 0: I S A escribe una vez en x y SB lee una vez de x. I El estado final solo depende del orden entre los dos accesos a x (no importa el orden de los accesos a registros y las variables locales). I Por tanto únicamente hay dos posibles estados finales. I Si se lee x y luego se escribe, al final b==1. I Si se escribe x y luego se lee, al final b==2. En la siguiente diapositiva vemos dos trazas que dan lugar a los dos valores de b posibles. Escribe, el resto de trazas y verifica que el valor final solo depende del orden de los accesos a x. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 48 de 91. Ejemplo de solapamiento de instrucciones atómicas (2/2) Vemos dos trazas que dan lugar a los dos valores de b posibles: PA PB rA a rB b x - 0 - 0 0 r A := a 0 0 - 0 0 x := r A +1 0 0 - 0 1 rB := x 0 0 1 0 1 b := rB +1 0 0 1 2 1 PA PB rA a rB b x - 0 - 0 0 r A := a 0 0 - 0 0 rB := x 0 0 0 0 0 x := r A +1 0 0 0 0 1 b := rB +1 0 0 0 1 1 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 49 de 91. Solapamiento de sentencias atómicas En general, si suponemos que dos procesos secuenciales distintos ejecutan concurrentemente cada uno de ellos una sentencia atómica cualquiera (S0 uno y S1 el otro), a partir de una estado E, entonces: I Puesto que S0 y S1 son atómicas, la ejecución concurrente de ambas es equivalente a la secuencial, es decir el estado posterior siempre será uno cualquiera de estos dos: I Estado resultado de ejecutar S0 completa, seguida de S1. I Estado resultado de ejecutar S1 completa, seguida de S0. Es decir: si S0 y S1 son ambas atómicas, entonces cada vez que se ejecuta la sentencia S0 kS1 el resultado será equivalente a ejecu- tar S0 ;S1 o bien a ejecutar S1 ;S0. Por tanto, en general, podemos analizar el comportamiento de un programa concurrente suponiendo que las instrucciones atómicas no se solapan (aunque realmente sí lo hagan). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 50 de 91. Interfoliación de sentencias atómicas Supongamos un programa concurrente C con dos procesos secuenciales, I uno ejecuta la secuencia de instr. atómicas A1 A2 A3 A4 A5 , I y otro ejecuta la secuencia de instr. atómicas B1 B2 B3 B4 B5. Entonces, al ejecutar el programa concurrente C, puede ocurrir cualquier interfoliación de sentencias atómicas que respete el orden dentro de cada proceso secuencial. Aquí vemos algunos ejemplos de interfoliaciones posibles: A1 A2 A3 A4 A5 B1 B2 B3 B4 B5 B1 B2 B3 B4 B5 A1 A2 A3 A4 A5 A1 B1 A2 B2 A3 B3 A4 B4 A5 B5 B1 B2 A1 B3 B4 A2 B5 A3 A4 A5 ··· Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 51 de 91. El número de posibles interfoliaciones El proceso P1 ejecuta n1 instr. atómicas, y el proc. P2 ejecuta n2 : I Hay tantas posibles interfoliaciones de P1 y P2 como posibles subconjuntos (de n1 elementos) del conjunto {1, 2,... , n1 + n2 } (es igual si consideramos subconjuntos de n2 elementos). Luego el núm. de interfoliaciones es este coeficiente binomial: ! n1 + n2 ( n1 + n2 ) ! = n1 n1 ! n2 ! I Si tenemos k procesos se usa el coeficiente multinomial: ! n1 + n2 + · · · + n k ( n1 + n2 + · · · + n k ) ! = n1 , n2 ,... , n k n1 ! n2 ! · · · n k ! I Por ejemplo, para n1 = 10 y n2 = 15 hay 3.286.760 interf. Conclusión: el número de posibles interfoliaciones es muy ele- vado incluso para programas cortos Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 52 de 91. Abstracción El modelo basado en el estudio de todas las posibles secuencias de ejecución entrelazadas de los procesos constituye una abstracción: I Se consideran exclusivamente las características relevantes que determinan el resultado del cálculo I Esto permite simplificar el análisis y diseño de los programas concurrentes. Se ignoran los detalles no relevantes para el resultado, por ejemplo: I Las áreas de memoria asignadas a los procesos. I Los registros particulares que están usando. I El costo de los cambios de contexto entre procesos. I La política del S.O. relativa a asignación de CPU. I Las diferencias entre entornos multiprocesador o monoprocesador. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 53 de 91. Velocidad de ejecución. Hipótesis del progreso finito. Progreso Finito No se puede hacer ninguna suposición acerca de las velocidades absolutas/relativas de ejecución de los procesos, salvo que es mayor que cero. Un programa concurrente se entiende en base a sus componentes (procesos) y sus interacciones, sin tener en cuenta el entorno de ejecución. Ejemplo: Un disco es normalmente más lento que una CPU, pero no podemos suponer que siempre es así para diseñar un programa. Si se hicieran suposiciones temporales: I Sería difícil detectar y corregir fallos I La corrección dependería de la configuración de ejecución, que puede cambiar Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 54 de 91. Hipótesis del progreso finito Si se cumple la hipótesis, la velocidad de ejecución de cada proceso será no nula, lo cual tiene estas dos consecuencias: Punto de vista global Durante la ejecución de un programa concurrente, en cualquier momento existirá al menos 1 proceso preparado, es decir, even- tualmente se permitirá la ejecución de algún proceso. Punto de vista local Cuando un proceso concreto de un programa concurrente co- mienza la ejecución de una sentencia, completará la ejecución de la sentencia en un intervalo de tiempo finito. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 55 de 91. Notación para expresar ejecución concurrente. Tipos. Usaremos una notación (la llamamos pseudo-código) para expresar el código y la sincronización de los distintos procesos secuenciales que forman un programa concurrente. Distinguimos dos tipos de sistemas concurrentes en función de las posibilidades para especificar cuáles son sus procesos: Sistemas Estáticos I Número de procesos fijado en el fuente del programa. I Los procesos se activan al lanzar el programa. I Ejemplo: Message Passing Interface (MPI-1). Sistemas Dinámicos I Número variable de procesos/hebras que se pueden activar en cualquier momento de la ejecución. I Ejemplos: OpenMP, PThreads, Java Threads, MPI-2. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 56 de 91. Grafo de Sincronización Un Grafo de Sincronización es un Grafo Dirigido Acíclico (DAG) donde cada nodo representa una secuencia de sentencias del programa (una actividad). P0 Dadas dos actividades A y B, una P1 P2 P3 P4 arista (flecha) desde A hacia B sig- nifica que B no puede comenzar su P5 P6 ejecución antes de que A termine. P7 El grafo muestra las restricciones de precedencia que determinan cuándo una actividad puede empezar en un programa. Ejemplo: B lee una variable compartida que ha debido ser escrita antes por A. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 57 de 91. Definición estática de procesos El número de procesos (arbitrario) y el código que ejecutan no cambian entre ejecuciones. Cada proceso se asocia con su identificador y su código mediante la palabra clave process.   var... { vars. compartidas } process NomUno ; var... { vars. locales } inicio begin.... { código } end NomUno NomDos process NomDos ; var.... { vars. locales } begin.... { codigo } fin end... { otros procesos }   El programa acaba cuando acaban todos los procesos. Las vars. compartidas se inicializan antes de que comienzen los procesos. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 58 de 91. Definición estática de vectores de procesos Se pueden usar definiciones estáticas de grupos de procesos similares que sólo se diferencian en el valor de una constante (vectores de procesos)   var... { vars. compartidas } process NomP[ ind : a..b ] ; inicio var... { vars. locales } begin..... { código } NomP[a].... NomP[b]..... { (ind vale a, a + 1,... , b) } end fin... { otros procesos }   I En cada caso, a y b se traducen por dos constantes concretas (el valor de a será típicamente 0 ó 1). I El número total de procesos será b − a + 1 (se supone que a. I Sea S una sentencia cualquiera, entonces < S > es otra sentencia equivalente a S pero que es atómica por definición. I Aquí equivalente significa que hace los mismos accesos a memoria y los mismos cálculos que S. I Los cambios de estado que pueda hacer < S > en variables compartidas ocurren aparentemente de una sola vez para los otros procesos secuenciales. La sentencia < S > es de un nuevo tipo de sentencia atómica, ya que puede hacer más de un acceso a variables compartidas, pero los posibles estados intermedios de esas variables compartidas no son accesibles a los otros procesos secuenciales. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 72 de 91. Ejemplo de sentencias atómicas Aquí vemos, a modo de ejemplo, dos sentencias concurrentes parecidas, excepto que la de la derecha usa la notación que se acaba de introducir (la variable x es compartida):     { instr. no atómicas } { instr. atómicas } begin begin x := 0 ; x := 0 ; cobegin cobegin x:= x+1 ; < x:= x+1 > ; x:= x-1 ; < x:= x-1 > ; coend coend end end     I En el código de la izquierda, al acabar, x puede tener un valor cualquiera del conjunto {−1, 0, 1}. I A la derecha, x finaliza con seguridad con el valor 0. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 73 de 91. Actividad de clase (1/2) Otro ejemplo sería un programa concurrente en el cual varios procesos comparten dos variables enteras x e y, y queremos que siempre se cumpla x+y == 10. Dado un valor n cualquiera (puede ser una constante o una variable local), para asignarle n a la variable x (y actualizar adecuadamente y) podríamos usar alguna de estas tres sentencias alternativas:       { Opción 1 } { Opción 2 } { Opción 3 } begin begin begin x:= n; ; < x:= n; y:= 10-n; ; y:= 10-n; > end end end       Para cada opción: describe razonadamente si, al ejecutarse la sentencia bloque en un estado previo con x+y==10, se garantiza que siempre en el estado posterior se cumplirá x+y==10. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 74 de 91. Actividad de clase (2/2) Para verificar que la suma de ambas variables siempre es 10, escribimos código que imprime dicha suma. Usamos una variable local a y alguna de las siguientes sentencias alternativas:       { Opción 1 } { Opción 2 } { Opción 3 } begin begin begin a:= x+y; < a:= x+y >; < a:= x+y; print(a); print(a); print(a); > end end end       Para cada opción: describe razonadamente si, al ejecutarse la sentencia bloque en un estado previo con x+y==10, se garantiza que siempre se imprimirá el valor 10. Además: ¿ es atómica la sentencia begin-end de la opción 2 ? Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 75 de 91. Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 3. Exclusión mutua y sincronización Subsección 3.2. Condición de sincronización. Condición de sincronización. En general, en un programa concurrente compuesto de varios procesos, una condición de sincronización establece que: no son correctas todas las posibles interfoliaciones de las secuencias de instrucciones atómicas de los procesos. I esto ocurre típicamente cuando, en un punto concreto de su ejecución, uno o varios procesos deben esperar a que se cumpla una determinada condición global (depende de varios procesos). Veremos un ejemplo sencillo de condición de sincronización en el caso en que los procesos puedan usar variables comunes para comunicarse (memoria compartida). En este caso, los accesos a las variables no pueden ordenarse arbitrariamente (p.ej.: leer de ella antes de que sea escrita) Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 77 de 91. Ejemplo de sincronización. Productor-Consumidor Un ejemplo típico es el de dos procesos cooperantes en los cuales uno de ellos (productor) produce una secuencia de valores (p.ej. enteros) y el otro (consumidor) usa cada uno de esos valores. La comunicación se hace vía la variable compartida x:   { variables compartidas } var x : integer ; { contiene cada valor producido }       { Proceso productor: calcula 'x' } { Proceso Consumidor: lee 'x' } process Productor ; process Consumidor ; var a : integer ; { no compartida } var b : integer ; { no compartida } begin begin while true do begin while true do begin { calcular un valor } { leer de mem. compartida } a := ProducirValor() ; b := x ; { sentencia L } { escribir en mem. compartida } { utilizar el valor leido } x := a ; { sentencia E } UsarValor(b) ; end end end end     Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 78 de 91. Secuencias correctas e incorrectas Los procesos descritos solo funcionan como se espera si el orden en el que se entremezclan las sentencias elementales etiquetadas como E (escritura) y L (lectura) es: E, L, E, L, E, L,.... I L, E, L, E,... es incorrecta: se hace una lectura de x previa a cualquier escritura (se lee valor indeterminado). I E, L, E, E, L,... es incorrecta: hay dos escrituras sin ninguna lectura entre ellas (se produce un valor que no se lee). I E, L, L, E, L,... es incorrecta: hay dos lecturas de un mismo valor, que por tanto es usado dos veces. La secuencia válida asegura la condición de sincronización: I Consumidor no lee hasta que Productor escriba un nuevo valor en x (cada valor producido es usado una sola vez). I Productor no escribe un nuevo valor hasta que Consumidor lea el último valor almacenado en x (ningún valor producido se pierde). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 79 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 4. Propiedades de los sistemas concurrentes. Concepto de corrección de un programa concurrente Propiedad de un programa concurrente: Atributo del programa que es cierto para todas las posibles secuencias de interfoliación (historias del programa). Hay 2 tipos: I Propiedad de seguridad (safety). I Propiedad de vivacidad (liveness). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 81 de 91. Propiedades de Seguridad (Safety) Son condiciones que deben cumplirse en cada instante, del tipo: nunca pasará nada malo. I Requeridas en especificaciones estáticas del programa. I Son fáciles de demostrar y para cumplirlas se suelen restringir las posibles interfoliaciones. Ejemplos: I Exclusión mutua: 2 procesos nunca entrelazan ciertas subsecuencias de operaciones. I Ausencia Interbloqueo (Deadlock-freedom): Nunca ocurrirá que los procesos se encuentren esperando algo que nunca sucederá. I Propiedad de seguridad en el Productor-Consumidor: El consumidor debe consumir todos los datos producidos por el productor en el orden en que se van produciendo. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 82 de 91. Propiedades de Vivacidad (Liveness) Son propiedades que deben cumplirse eventualmente, del tipo: realmente sucede algo bueno. I Son propiedades dinámicas, más difíciles de probar. Ejemplos: I Ausencia de inanición (starvation-freedom): Un proceso o grupo de procesos no puede ser indefinidamente pospuesto. En algún momento, podrá avanzar. I Equidad (fairness): Tipo particular de prop. de vivacidad. Un proceso que desee progresar debe hacerlo con justicia relativa con respecto a los demás. Más ligado a la implementación y a veces incumplida: existen distintos grados. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 83 de 91.  Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 5. Verificación de programas concurrentes. 5.1. Introducción 5.2. Enfoque axiomático. Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 5. Verificación de programas concurrentes Subsección 5.1. Introducción. Introducción. Pruebas simples. Limitaciones. ¿ Cómo demostrar que un programa cumple una determinada propiedad ? I Posibilidad: realizar diferentes ejecuciones del programa y comprobar que se verifica la propiedad. I Problema: Sólo permite considerar un número limitado de historias (interfoliaciones) de ejecución y no demuestra que no existan casos indeseables. I Ejemplo: Comprobar que el proceso P produce al final x = 3:   process P ; var x : integer := 0 ; cobegin x := x+1 ; x := x+2 ; coend   (hay varias historias que llevan a x==1 o x==2, pero estas historias podrían no ocurrir en unas pocas ejecuciones). Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 86 de 91. Enfoque operacional (análisis exhaustivo) I Enfoque operacional: Análisis exhaustivo de casos. Se chequea la corrección de todas las posibles historias. I Problema: Su utilidad está muy limitada cuando se aplica a programas concurrentes complejos ya que el número de interfoliaciones crece exponencialmente con el número de instrucciones de los procesos. I Para el sencillo programa P (2 procesos, 3 sentencias atómicas por proceso) habría que estudiar 20 historias diferentes. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 87 de 91. Sistemas Concurrentes y Distribuidos, curso 2024-25. Tema 1. Introducción. Sección 5. Verificación de programas concurrentes Subsección 5.2. Enfoque axiomático.. Verificación. Enfoque axiomático. I Se define un sistema lógico formal que permite establecer propiedades de programas en base a axiomas y reglas de inferencia. I Se usan fórmulas lógicas (asertos) para caracterizar un conjunto de estados. I Las sentencias atómicas actúan como transformadores de predicados (asertos). Los teoremas en la lógica tienen la forma: { P} S { Q} “Si la ejecución de la sentencia S empieza en algún estado en el que es verdadero el predicado P (precondición), entonces el predicado Q (poscondición) será verdadero en el estado resultante.” I Menor Complejidad: El trabajo que conlleva la prueba de corrección es proporcional al número de sentencias atómicas en el programa. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 89 de 91. Invariante global I Invariante global: Predicado que referencia variables globales siendo cierto en el estado inicial de cada proceso y manteniéndose cierto ante cualquier asignación dentro de los procesos. I En una solución correcta del Productor-Consumidor, un invariante global sería: consumidos ≤ producidos ≤ consumidos + 1 Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 90 de 91. Bibliografía del tema 1. Para más información, ejercicios, bibliografía adicional, se puede consultar: 1.1. Conceptos básicos y Motivación Palma (2003), capítulo 1. 1.2. Modelo abstracto y Consideraciones sobre el hardware Ben-Ari (2006), capítulo 2. Andrews (2000) capítulo 1. Palma (2003) capítulo 1. 1.3. Exclusión mutua y sincronización Palma (2003), capítulo 1. 1.4. Propiedades de los Sistemas Concurrentes Palma (2003), capítulo 1. 1.5. Verificación de Programas concurrentes Andrews (2000), capítulo 2. Sistemas Concurrentes y Distribuidos- Curso 2024-25- Creado: 18 de septiembre de 2024 – transparencia 91 de 91. Fin de la presentación.