Home » forums » LtU Forum

Holistic types

(This is a revision of an earlier post)

The holistic types can be used to enforce safe access
to objects in a multi-threading environment. Another
potential application is to support object swapping
between primary and secondary storage.

Objects of the holistic types cannot be accessed directly
through the references. Read and write access is only
permitted via special read/write references. Obtaining
a read/write reference implicitly locks the object.
Read/write reference cannot be stored inside an object
since the assignment would drop the read/write qualifier.
So, it is impossible to pass a read/write object reference
to another execution context (process/thread).

Type modifier for object declaration:

 holistic

It is not allowed to use a simple reference to an
object of a holistic type to read or modify its contents.
If a holistic type A refers to a non-primitive type
B then B must be holistic.

Type modifiers for reference declaration:

 read

 write

References with the resulting types are used to actually
read and modify the holistic objects.

They can be obtained through locking:

 rlock: holistic -> read

 wlock: holistic -> write

Read/write reference looses the modifier upon assignment to an object field:

 assignment to a field: read/write -> holistic

Since the read/write references cannot be stored, we
do not need to deal to circular references. This allow us
to control the scopes of locks by standard reference
counting.

By Igor Serikov at 2011-01-28 17:09 | LtU Forum | previous forum topic | next forum topic | other blogs | 5391 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

If a holistic type A refers

If a holistic type A refers to a non-primitive type B then B must be holistic.

Then how do you ever wrap a non-primitive T in a holistic[T] in the first place?

Since the read/write references cannot be stored, we
do not need to deal to circular references [of locks]. This allow us
to control the duration of the locking by standard reference
counting.

You can still have deadlock patterns. Alice locks A then B. Bob locks B then A. It is unclear to me how you can control duration of locks without first solving the deadlock problem. (Similarly, a procedure could lock an object then enter an infinite loop due to a bug.)

What problem, precisely, is being solved by these holistic types?

By dmbarbour at Fri, 2011-01-28 18:10 | login or register to post comments

Then how do you ever wrap a

Then how do you ever wrap a non-primitive T in a holistic[T] in the first place?

It is a type and can be supported through a compiler or rewriter.

It is unclear to me how you can control duration of locks without first solving the deadlock problem.

"duration" was a bad word. It should be "scope".

What problem, precisely, is being solved by these holistic types?

The purpose is enforcing access policy as stated.
Why is it important?
For example, a statement like "o.v = o.v + 2;" would always work as expected. The programmer would still be able to write an incorrect program but he would have to work harder to achieve it. Yet, we no longer need to provide special handling for non-atomic assignments/extractions.

By Igor Serikov at Sat, 2011-01-29 10:26 | login or register to post comments

You might want to look at

You might want to look at related systems in both security and concurrency literature, e.g., SharC, Plaid, etc.

By lmeyerov at Fri, 2011-01-28 19:21 | login or register to post comments

I keep doing it:) But thank

I keep doing it:)
But thank you for the pointers.

By Igor Serikov at Sat, 2011-01-29 09:38 | login or register to post comments

If you are, it'd help PL

If you are, it'd help PL people knowledgeable in these areas if you more explicitly discuss what you're doing and with the standard terminology. Sharing is an important area for many domains, so it's hard to point to something specific without more. Otherwise, you get random replies, as we're observing.

By lmeyerov at Sat, 2011-01-29 19:47 | login or register to post comments

I changed the subject to

I changed the subject to avoid confusion with the security-related things and to narrow the problem scope. But willingness of some people to read beyond the subject line is nonetheless highly appreciable:)

By Igor Serikov at Sun, 2011-01-30 11:44 | login or register to post comments

Static locking

If you place constraints on lock access into the type system then you are insisting that the access patterns can be resolved statically - your type system is simply a program running at compile time to evaluate the locking order. This won't work on all programs, as there are some kinds of locking patterns that might depend on dynamic data. Working out what set of programs you can write in this way, and what set you cannot, would be quite an interesting result.

I'd recommend sexy types as some background material. The relevance is that you are trying to control some low-level observable state through the type system. There are also some related results in resource access control - similar additions to a type system to arbitrate access to various resources, files, sockets etc. Lots of work turns up in the context of mobile/embedded systems.

The problem is pointed out by dmbarbour in the earlier post. It is not clear exactly which problem you think that you are solving. You pointed him back to "A type system that enforces object sharing policies", but this doesn't answer the question. What object sharing policy, and how does it enforce it? If your policy is too "strong" or "precise" and you want to enforce it strictly then you will run into the deadlock avoidance problem. If you weaken your enforcement to avoid this problem then it becomes important to know exactly how you weaken it (what sort of behaviour you tolerant) as it changes your system drastically.

Based on exactly what you are trying to achieve, previous work in this area has generally proceeded by adding a static analysis on-top of the type system. The type checker gives you a guarantee about some properties of the lock usage/discharge and then the static analysis rules out further undesirable behaviours. But to know how much of one, or the other, you require you need to specify what you are trying to achieve.

By Andrew Moss at Sat, 2011-01-29 11:47 | login or register to post comments

Region-based locking, Cyclone

If we're dealing with safe locking, there's been plenty of work on region-based locking, primarily from the Cyclone group. Here's a Google search for a number of these papers.

By naasking at Sat, 2011-01-29 16:31 | login or register to post comments

Vault?

This resembles the Vault type system.

Adoption and Focus: Practical Linear Types for Imperative Programming (PLDI '02)

Also, Phillip Haller's Scala page has some nice work on capabilities for uniqueness types.

By Sriram Srinivasan at Tue, 2011-02-01 15:37 | login or register to post comments