Plessey System 250 , también conocido como PP250, fue la primera computadora operativa en implementar direccionamiento basado en capacidades , para verificar y equilibrar el cálculo como una máquina pura de Church-Turing .
La máquina A Church-Turing es un ordenador digital que encapsula los símbolos en un hilo de cálculo como una cadena de abstracciones protegidas mediante la aplicación de las leyes de la unión dinámica Alonzo Church 's cálculo lambda [1] a otros ordenadores basados capacidad, que incluyen CHERI y CAP las computadoras , son híbridos. Conservan las instrucciones predeterminadas que pueden acceder a cada palabra de la memoria física o lógica (paginada) accesible. [ cita requerida ]
Es una característica inevitable de la arquitectura de von Neumann [ cita requerida ] que se basa en la memoria compartida de acceso aleatorio y la confianza en los derechos de acceso predeterminados compartidos. Por ejemplo, cada palabra en cada página administrada por el administrador de memoria virtual en un sistema operativo que usa una unidad de administración de memoria (MMU) debe ser confiable. [ cita requerida ] El uso de un privilegio predeterminado entre muchos programas compilados permite que la corrupción aumente sin ningún método de detección de errores. Sin embargo, el rango de direcciones virtuales dadas a la MMU o el rango de direcciones físicas producidas por la MMU son flujos de corrupción no detectados compartidos a través del espacio de memoria compartida de una función de software a otra. [cita requerida ]PP250 eliminó no solola memoria virtual[1]sistema operativocentralizado precompilado, sino también elsuperusuario, eliminando todos los privilegios predeterminados de la máquina.
Son los privilegios predeterminados los que habilitan el malware y la piratería no detectados en una computadora. En cambio, el modelo de capacidad de objeto puro de PP250 siempre requiere una clave de capacidad limitada para definir la autoridad para operar. PP250 separó los datos binarios de los datos de capacidad para proteger los derechos de acceso, simplificar la computadora y acelerar la recolección de basura . La máquina de la Iglesia encapsula y el contexto limita la máquina de Turing al hacer cumplir las leyes del cálculo lambda . Los medios digitales mecanografiados están controlados por programa mediante instrucciones de máquina claramente diferentes .
Los datos binarios mutables se programan mediante un conjunto de instrucciones RISC de 28 para la programación imperativa y la programación procedimental de los datos binarios utilizando registros de datos binarios confinados a un segmento de memoria de capacidad limitada. Las teclas de capacidad inmutables, exclusivas de seis instrucciones de Church, navegan por el contexto computacional de una máquina de Turing a través de la estructura programada por separado del modelo de capacidad de objeto .
Las claves de capacidad inmutables representan variables de cálculo lambda con nombre. Este lado de la Iglesia es un cálculo lambdameta-máquina. El otro lado es una máquina orientada a objetos de objetos binarios, funciones programadas, listas de capacidad que definen abstracciones de funciones, almacenamiento para hilos de cálculo (aplicaciones de cálculo lambda) o almacenamiento para la lista de claves de capacidad en un espacio de nombres. Las leyes del cálculo lambda son implementadas por las instrucciones de la Iglesia con acceso microprogramado a los registros de capacidad reservados (ocultos). El software se ensambla gradualmente como código de máquina orientado a objetos vinculado por las claves de capacidad. La estructura de las abstracciones de funciones, incluidas las de gestión de memoria, entrada y salida, programación y servicios de comunicación, están protegidas como tramas privadas en un hilo. Hilos de computadora en línea o como cálculos paralelos activados por instrucción de la Iglesia controlada por programa.