nondeterministic . net

Notes from Semantics and its Applications Workshop, December 19, Tel Aviv University.

Process Extraction in a Logic of Events

Semantic Issues in the Definition of a Hardware Specification Language

Semantics of Communication Systems

A Logic of Reachable Patterns in Linked Data-Structures

Lunch

Socially Responsive Environmentally Friendly Logic

Hennessy-Plotkin-Brookes Revisited

Language Features for Program Monitoring

Notes are sometimes serious, sometimes not. There were British folk involved, so, you know. No editing has been done. No links, either; Google as needed. Continues tomorrow, with lectures more (at least theoretically) interesting to me. Maybe I’ll even format those notes better.

Process Extraction in a Logic of Events

Robert L. Constable, Cornell University

with Mark Bickford

Introduction

Some fashionable Microsoft bashing

Looking for close connection between code and semantic specification

Event Structures

Signatures and Axioms

Smart people like events, so we like them, too

Events at multiple locations

Event predecessors within a location

Event senders at another location (if event is a receive)

Example Specifications

The following is easy to read:

Process Extraction from Proofs

Extract an entire distributed system from a proof

Let’s recall functional program synthesis

Given a proof using constructive logic, can construct a program

Refinements for systems

system D s.t. event structures es, we have R(es)

Prove this; synthesize program from the proof

Example:

Relate send events to knowledge, create a boolean variable

Require ready to be true before sends, false after

Write some lemmas

Lemmas give us the r event that resets ready

Set up the world to satisfy lemmas

Limit sending actions, add precondition

Limit actions that can affect certain variables (frame condition)

By unioning constraints, result is a two-way handshake automaton, which is convertable to Java

Questions

Some points about conflicting events, and questions about so-and-so’s something-or-other

Semantic Issues in the Definition of a Hardware Specification Language

Cindy Eisner, IBM Haifa Research Lab

The problem

Define abort operator: for boolean b iff up to the point of b, nothing has gone wrong

Intuition: take some automaton for and add an escape on b

Why not with until: consider (Fp) abort q vs (Fp) U q, where p never happens

LTL

Elegant but “wrong” semantics

What’s wrong? Consider true U false

Automaton with escape on b captures correct notion

But we don’t have j, w’

What else is wrong? Non-elementary complexity

Desired but ugly semantics

ForSpec accept operator

Correct, computational complexity OK, but ugly

Truncated semantics

Defined with different goal: use of temporal logic on finite paths

Weak (-), neutral, and strong (+) views: what happens to properties when paths end

Define finite words followed by epsilons

Define operators for each view (negation for one uses the other)

Truncated semantics and abort operator

Abort operator truncates the path and switches to weak view (from any starting view)

Better

Add and where for any b, including false

With this change: elegant but “wrong” semantics are now right

Prove using truncated semantics

Conclusion

Changing the alphabet changes the complexity

Semantics of Communication Systems

Gideon Ariely, Israeli Ministry of Science

Communication between Agents

Alice and Bob communicate via a stream of symbols

Syntax (symbols), semantics (meaning), implementation (realization)

Eve has taken 6.095 and feels strangely compelled to disrupt their communication

OSI Model

Application - Presentation - Session - Transport - Network - Data-Link - Physical

Programming Constructs

Distinction between syntax, semantics, and implementation

Back to OSI

Need to define and formalize new concepts as more is abstracted

A Logic of Reachable Patterns in Linked Data-Structures

Greta Yorsh

with Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani

Heap-Manipulating Programs

Imperative languages, arbitrary heap size and structure, destructive pointer updates

Reachability invariants, data-structure invariants temporarily violated

Specification Language

Reachablilty (identify garbage, disjoint, acyclic)

Also data-structure and loop invariants

Decidable

Natural choices (FO, FO+TC, or MSO, of course) are undecidable

Guarded fixpoints, EADTC, , or MSO on trees

Problems with Monadic Second-Order Logic limited to trees

Not expressive for many desired formulas

May not be working on trees (or temporarily break a tree during an operation)

Logic of Reachable Patterns

Balance between complex structures and complex properties

Fragment is decidable

Logic of Reachable Patterns

Background

Heap as directed labeled graph

c[R]p: from c, if you take an R path, then the destination satisfies p

Pattern p: consists of neighborhood formula N and quantifier-free formula

Routing expression R: forward and backward edge traversal, and marking

Define , x=y, and

“Paths in the heap that reach a pattern”

Interesting Heap Properties

Too many symbols I don’t know how to off the top of my head

Reachability, cyclicity, and disjointness

Cyclicity is not a word

Define to capture unshared structure

Use to define a tree rooted at a certain node

Other structures also expressible

Well-Formed Heap: all fields are deterministic, pointing to only one location

Loop invariant for linked-list reversal

Satisfiability of LRP is undecidable

Ain’t it always the way

Idea: enforcing existence of edges can reduce to deciding TM behavior

Issue is ability to talk about far away nodes

Fragment

Restrict the patterns p in c[R]p

Equality patterns: neighborhood formula only looks within distance two and implies equality

Edge patterns: neighborhood formula looks only within distance one and implies an edge

Negative patterns: neighborhood formula implies any negative

All previous examples were actually in

Whoopie!

“Paths in the heap that reach a pattern if you’re short-sighted”

Verification Conditions

Can generate verification condition in given pre- and postconditions and loop invariants in

Works with arbitrary pointer modifications

Decidability of

Closed under negation, show satisfiability decidable, use tree-like graphs

Worst-case complexity is doubly-exponential

Questions

Quantification is implicitly universal

Modal logic can’t capture sharing; here we can, but only at limited distance

Hypered logics something something

Lunch

Socially Responsive Environmentally Friendly Logic

Samson Abramsky, Oxford University Computing Laboratory

British humor, ha ha

Introduction

Question: what kind of logic has a natural semantics in multi-agent games?

Usually connections between games and logic use 2-person games

Quantifiers

The 1959 Henkin Quantifier

I’m not ing that, either

IF quantifier: linearlization

From 2-person games to n-person games

Naturalness of 2-person games: correlates to polarity, domain and codomain, and co- and contra-variance

iff the verifier has a winning strategy in the game

Aside

Note that is translated to

No information flow between predicate and consequent

Various definitions

British humor clashes with Russian directness

Semantics of

Static: assign games to formulas

Dynamic: define strategies and strategy profiles

Concrete data structures as concurrent games

Food coma

Questions

Can you give some intuition? Well, no

No really, can you? Well, yes

Can you describe coalitions?

Are there any coalitions worth describing nowadays?

Hennessy-Plotkin-Brookes Revisited

Gordon Plotkin, School of Informatics, Laboratory for Foundations of Computer Science, University of Edinburgh

Overhead slides!

Work influence from 1976; slides from the way over here on the plane

Presentation assumes knowledge of monads, theories, and something else I don’t know what it is

Ergo, good luck getting anything out of these notes

Oh the British humor

Simple Imperative Parallel Programming Language

when b do p: evaluating b is atomic along with, if true, the first action of p

P or Q: nondeterministic choice

Operational semantics and rules

Question about missing primes: “yeah basically I was hoping you wouldn’t notice that”

Resumption Semantics

“Mathematical microcode”

Question: is there some weird thing you can do to something something? Oh, that would be weird, and this other thing would be weirder

Monads and Semantics

This part will be high speed, in strong contrast to the previous parts

We’re also skipping technicalities, apparently

Write down seven fun equations (that even I could actually understand) and you have a complete description of state (monads are the free algebra)

Equation Theories and Semantics

Trace-Based Semantics - Brookes

Basic finite traces model of parallel programming

Traces are finite sequences of actions, a “little bit” of a resumption

Algebra with delay, lookup, update

Brookes Rules

Stuttering: problem with when operator, solved by not stuttering on nothing

Mumbling

Language Features for Program Monitoring

Oege de Moor, Programming Tools Group, Oxford University, Computing Laboratory

with a long list of people

Aspect-Oriented Programming

Static: inject new members into existing classes at compile time

Dynamic: aspects observe composite events in base program; run extra code at begin/end of certain events

Terminology

Joinpoint: composite event = node in generalized dynamic call graph

Pointcut: patter of events = set of nodes in call graph

Advice: extra code

Shadow: program point (code) that corresponds to joinpoint

Advice can be run before, after, or around a joinpoint

Example Aspects

NoNewInRound: No allocations with “new” in inner loop

before() : cflow(call(* World.play(..))) && call(*.new(..)) && !within(NoNewInRound) { System.err.println(”Bad alloc: ” + thisJoinPoint.getSourceLocation()); }

Memoisation

Integer around(Integer n) : call(Integer hardMethod() && args(n) { // proceed(n), put return in table with key n, and return it }

Tainted Strings

Check Strings coming from user control into critical methods (e.g. SQL injection)

Capturing String modifications and creations that transfer taintedness requires long disjunctive pointcut: problem is that pointcut is syntactic rather than semantic, where the notion is very clean

Tracematches (OOPSLA ‘05)

Alphabet declaration, regular pattern, and extra code

Filtering traces (no variables)

Example: autosave

Example: observing an oblivious object

tracematch(Subject s, Observer o) for parameterization

Sequence of enter/exists is filtered for every instantiation of free variables, check for pattern match, if so run code

Example: failsafe enumeration over Vectors

create_enum call_next* update_source+ call_next

Example: constant hashcodes

Use let in symbol declaration to remember old hashcode

Declare symbol remove, but pattern is “add contains,” to force no remove operation between add and contains

Operation Semantics

Run state machine alongside program

States tagged with constraints

Equality

Inequality: if you “skip” an event that might match with (v=o), you must assume ()

Theorem: declarative filtering semantics = constraint-based operational semantics

Problem: space leaks

Constrains maintained as propositions in disjunctive normal form

Cannot use weak references, but how long to hold on to an object?

Solution: classifying variable based on state as collectable, weak, or strong

Current Work: common special case where for variables A x and B y, for each x, there is exactly one y

Observer has one subject, enumeration has one Vector, etc.

Opportunities for Semantics

Clean model of aspects for any language

Language design and reasoning

Identify events by semantic properties

Information hiding

Expressive power of trace patterns

Implementation

Justify subtle use of weak references

Continuum from static to dynamic checking

Questions

Aspects in ML: two groups mentioned

JML

maxg

Both comments and trackbacks are closed.