Nancy S Lynch

US Patent:

62895028, Sep 11, 2001

Filed:

Mar 30, 1998

Appl. No.:

9/052396

Inventors:

Stephen J. Garland - Brookline MA
Nancy A. Lynch - Brookline MA

Assignee:

Massachusetts Institute of Technology - Cambridge MA

International Classification:

G06F 945

US Classification:

717 2

Abstract:

A new computer language, which is based on a formal, mathematical state-machine model, and which is used both to validate and to generate code for a distributed system, in general, enables developing a system using multiple related system specifications, for instance, using system specifications at multiple levels of abstraction or using multiple system decompositions into parallel combinations of interacting systems, and allows use of validation tools to verify properties of these systems and their relationships. The language includes constructs for specifying non-deterministic actions, and for specifying constraints on those non-deterministic choices. Several well-defined sub-languages of the full computer language are also defined. These sub-languages are used to specify the input of some tools, in particular, of some code generators. One method for developing a software implementation of a distributed system using the present invention includes accepting a design specification for the distributed system, and applying a validation procedure to the design specification to verify that the system has desired properties.

US Patent:

20180165318, Jun 14, 2018

Filed:

Dec 12, 2017

Appl. No.:

15/838966

Inventors:

- Cambridge MA, US
- Boston MA, US
- Farmington CT, US
Nancy Ann Lynch - Brookline MA, US
Erez Kantor - Brookline MA, US
Alexander Allister Schwarzmann - Storrs CT, US

International Classification:

G06F 17/30
H04L 29/08

Abstract:

Described are devices, systems and techniques for implementing atomic memory objects in a multi-writer, multi-reader setting. In an embodiment, the devices, systems and techniques use maximum distance separable (MDS) codes, and may be specifically designed to optimize a total storage cost for a given fault-tolerance requirement. Also described is an embodiment to handle the case where some of the servers can return erroneous coded elements during a read operation.