text:
|Publication number
|Publication type
|Application number
|Publication date
|Aug 10, 2010
|Filing date
|Jan 11, 2005
|Priority date
|Jan 11, 2005
|Fee status
|Also published as
|Publication number
|K. Rustan M. Leino, Wolfram Schulte, Bart Jacobs
|Original Assignee
|Microsoft Corporation
|Export Citation
|BiBTeX, EndNote, RefMan
|Patent Citations (36), Non-Patent Citations (57), Referenced by (14), Classifications (8), Legal Events (3)
|External Links: USPTO, USPTO Assignment, Espacenet
A portion of the disclosure of this patent document contains material which is subject to copyright protection. The copyright owner has no objection to the facsimile reproduction by any one of the patent disclosure, as it appears in the Patent and Trademark Office patent files or records, but otherwise reserves all copyright rights whatsoever.
The present invention relates generally to program checking tools that minimize potential unwanted interference among concurrent threads. The present invention relates particularly to a way to structure multi-thread object-oriented programs to guarantee that only one thread at a time can access an object.
A primary aim of a reliable software system is ensuring that all objects in the system maintain consistent states; that is, states in which all fields of an object, and all fields of other objects upon which it depends, contain legal, meaningful values. If an object contains only legal values, it is considered to maintain invariancy. It is difficult to maintain invariants in sequential programs, as an object invariant may temporarily be violated during the update of an object's data, and any method call performed during this time may potentially cause control to re-enter the object's public interface where the object invariant is expected to hold.
It is even harder in concurrent object-oriented programs. For example, consider a system where for all dual accounts, account a and account b are to sum to the value zero. Consider the code fragment shown below:
void Transfer(DualAccounts o, int amount) {
o.a := o.a − amount;
o.b := o.b + amount;
In a sequential setting, this code maintains the invariant. However, in a system where more than one thread is running concurrently, the invariant condition (a+b=0) can be violated. It is not possible for a program to change the values in o.a and o.b simultaneously, which allows for the possibility of invariant violation, and can also lead to inconsistent program behavior. Such inconsistencies are known as dataraces. A datarace occurs in an execution of a program where there are conflicting actions in multiple threads when the actions are not explicitly ordered.
One method to ensure invariancy is to guarantee that an individual update is atomic. That is, each update will be performed with no other code updates on other threads occurring until the operation is complete. This ensures that the value of o.a, for example, will not be changed while the line of code o.a:=o.a−amount is being processed. This is insufficient to prevent the invariancy from being violated, as an update to a or b could occur on a different thread between the subtraction and the addition steps.
For example,
One method used to ensure internal consistency in a multi-threaded environment is by enforcing atomicity of concurrent operations at a level coarser than individual reads and writes. Commonly, the objects being updated are locked using mutexes. The following procedure will ensure that, for the Transfer function below, invariancy would be maintained:
void Transfer(DualAccounts o, int amount) { Lock Mutex for o.a Lock Mutex for o.b o.a:=o.a − amount; o.b:=o.b + amount; Unlock Mutex for o.a Unlock Mutex for o.b }
However, mutex locks are expensive in terms of CPU time, and can cause other problems—such as starvation conditions, deadlocks, and race conditions; all of which can be very difficult to locate and debug, dependent as they are on very specific thread-statement ordering, such as that shown in
Extended Static Checkers for Modula-3 and for Java attempt to statically find errors in object-oriented programs. These tools include support for the prevention of dataraces and deadlocks. For each field, a programmer can designate which lock protects it. However, these two tools trade soundness for ease of use; for example, they do not take into consideration the effects of other threads between regions of exclusion. Moreover, various engineering trade-offs in the tools notwithstanding, the methodology used by the tools was never formalized enough to allow a soundness proof.
As described herein, a way to structure multi-thread object-oriented programs, which guarantees the absence of dataraces, is provided. The various techniques and tools can be used in combination or independently. The disclosed exemplary apparatus and methods should not be construed as limiting in any way. Instead, the present disclosure is directed toward novel and non-obvious features and aspects of the various disclosed embodiments, alone and in various combinations and subcombinations with one another. The methods are not limited to any specific aspect, feature, or combinations thereof, nor do the disclosed methods require that any one or more specific advantages be present or problems be solved.
One implementation comprises executing multiple threads on a computer; a specific thread t1 acquiring a lock on a top hierarchical object. Once an object is acquired, it can be unpacked, which changes ownership of the object to the thread t1. Only when a thread owns an object can it change any of the object's fields. When the thread acquires a lock on the top object all other threads are excluded from accessing the top object and any descendant objects.
In an exemplary embodiment, an object may be owned by either a thread, another object, or is free. The method may also comprise an invariant, where the invariant comprises legal values for at least two fields in two different objects. An object field may temporarily violate the invariant.
In some instances, if thread t1 owns the top object of an object hierarchy then thread t1 transitively owns all descendants of the top object and if thread t1 transitively owns an object then the method allows the thread t1 to read at least one object field from at least one descendant object; The thread t1 acquires ownership of a child object with a parent by unpacking the parent of the child object.
In another embodiment, which ensures that there are no dataraces between first and second unordered memory accesses within a multi-threaded program, a first and second memory access request must be owned by a single thread prior to performing the memory access requests. Owning, in this context, comprises the thread owning a common ancestor of objects requesting the memory accesses. These memory accesses may be at different memory locations, they may be declared as modified variables, and they may be declared as preconditions or postconditions in a routine in a computer program.
In a system implementation, the system comprises one thread with a thread table for determining object ownership. The system further comprises at least two objects hierarchically arranged. Each object may further consist of an owner field, which is used to determine the entity that owns the object, and at least one variable field. The system further consists of an object invariant condition which states legal values for the at least one variable field of at least one object; and a thread-object consistency module, which ensures that for each thread-object transition, the thread table indicates that the thread owns the new owned object and the object owner field indicates that the object is owned by the new owner thread. A writer module, which writes a value into the object variable field if the object is owned by the thread requesting write access, may also be present. This embodiment may also contain an invariant checker, which ensures that the object variable field contains the invariant condition legal values, and which is called after the writer module is accessed for a given object.
Additional features and advantages will be made apparent from the following detailed description of various embodiments that proceeds with reference to the accompanying drawings.
With reference to
A computing environment may have additional features. For example, the computing environment 200 includes storage 240, one or more input devices 250, one or more output devices 260, and one or more communication connections 270. An interconnection mechanism (not shown) such as a bus, controller, or network interconnects the components of the computing environment 200. Typically, operating system software (not shown) provides an operating environment for other software executing in the computing environment 200, and coordinates activities of the components of the computing environment 200.
The storage 240 may be removable or non-removable, and includes magnetic disks, magnetic tapes or cassettes, CD-ROMs, DVDs, or any other medium which can be used to store information and which can be accessed within the computing environment 200. The storage 240 stores instructions for the software 280 implementing the mechanisms to aid in the verification of multi-threaded object-oriented programs with invariants.
The input device(s) 250 may be a touch input device, such as a keyboard, mouse, pen, or trackball, a voice input device, a scanning device, or another device that provides input to the computing environment 200. For audio or video encoding, the input device(s) 250 may be a sound card, video card, TV tuner card, or similar device that accepts audio or video input in analog or digital form, or a CD-ROM or CD-RW that reads audio or video samples into the computing environment 200. The output device(s) 260 may be a display, printer, speaker, CD-writer, or another device that provides output from the computing environment 200.
The communication connection(s) 270 enable communication over a communication medium to another computing entity. The communication medium conveys information, such as computer-executable instructions, audio or video input or output, or other data in a modulated data signal. A modulated data signal is a signal that has one or more of its characteristics set or changed in such a manner as to encode information in the signal. By way of example, and not limitation, communication media include wired or wireless techniques implemented with an electrical, optical, RF, infrared, acoustic, or other carrier.
The techniques and tools can be described in the general context of computer-readable media. Computer-readable media are any available media that can be accessed within a computing environment. By way of example, and not limitation, with the computing environment 200, computer-readable media include memory 220, storage 240, communication media, and combinations of any of the above.
The techniques and tools can be described in the general context of computer-executable instructions, such as those included in program modules, being executed in a computing environment 200 on a target real or virtual processor. Generally, program modules include routines, programs, libraries, objects, classes, components, data structures, etc. that perform particular tasks or implement particular abstract data types. The functionality of the program modules may be combined or split between program modules as desired in various embodiments. Computer-executable instructions for program modules may be executed within a local or distributed computing environment 200.
If desired, the technologies described herein (i.e. verifying multi-threaded programs with invariants) can be provided as part of a program verification service. Programs interacting with the service can thus take advantage of the features as desired.
The various technologies described herein are useful to ensure that invariant values are preserved within a computer program.
For illustration purposes, invariants are discussed in terms of routines which are defined sections of code; an idea that encompasses functions, procedures, and other forms of code modulization as well. The examples given should be considered to be written in pseudo-code. It should be appreciated by those of skill in the art that the embodiments shown are not limited to any specific programming language.
In an exemplary embodiment, the data within a multi-threaded program is structured such that each object is either owned by a thread, owned by an object, or is free. Each thread has an ownership domain, which are the objects that the thread either owns or transitively owns. If an object is at the top of a hierarchy, it is either owned by a thread or is free. If a thread owns an object then it can change its values. It is understood that this embodiment can be used in a mixed environment; that is, there may be other ways for a thread to change the values of an object.
Data races are prevented in our methodology by 1) requiring that a thread own an object when it accesses one of its fields, and 2) ensuring that at no point during the execution do two threads own the same object. Therefore, two accesses by different threads of fields of the same object cannot occur concurrently (i.e. not-ordered) since this would mean that both threads own this object at the same time.
This relationship is shown in
Referring to
When the object is locked 506, any other threads that may be running are denied access to the locked object and to any descendants of the object, as shown at process block 510. With reference to
At process block 514, thread t1 unpacks the acquired top object; the ownership of any children of the top object is changed to the accessing thread. This ownership confers write access to the accessing thread of any objects that it owns; it can now modify their fields, as shown at process block 516. Ownership of the top hierarchical object grants the owning thread transitive ownership of all of the top hierarchical object's descendants, which allows the accessing thread to read their values, as shown at process block 512.
Turning now to
The exemplary structures shown in
Object 310 shows an exemplary embodiment of a portion of object from; it contains an owner field 315 which must hold the same value as the owner field of object t 320. As can be seen, the owner of from and to are both THREAD_A 330. The thread THREAD_A 330 must also have an indication that it owns both objects from 310 and to 320; the table OWNS 340 here does show both from 350 and to 360 being owned by the thread. The table structure 340 can be implemented using a hash table, pointers, a Boolean table, or any other reasonable method known to one of skill in the art.
Once it is verified that the current thread owns all of the designated objects, the body of the routine is performed. It should be noted that specifying a precondition does not cause a thread to acquire the objects mentioned therein, it just ensures that they must be acquired. Furthermore, acquiring an object doesn't change In the code example 600, the body of the routine contains two statements: from.Deposit(−amount) 650, and to.Deposit(amount) 655. These two statements will be executed in turn.
The class Account at 605 in
The Deposit routine 615 includes an postcondition 623, which states that the balance must equal the original balance when entering the routine (old(bal)) plus the amount of the variable passed into the routine (amount) 627. Furthermore, as Deposit 615 is a member of class Account 605, when it is packed it must maintain the invariant
Deposit 615 includes the precondition "requires inv" 620. The keyword "inv" is a boolean field that specifies whether or not the invariant declared for the object holds. Initially, upon creation of an object, inv is set to false. The statements pack 630 and unpack 625 switch the inv field on and off, respectively; unpack 625, therefore makes the object mutable which allows the object field values to be changed, while pack 630 marks the object as consistent—which prevents further modifications—provided that the new object field values do not violate the invariant. If the invariant is violated, then the program execution is aborted, in an exemplary embodiment by throwing an exception.
The body of Deposit 615 requires that the list hist 607 have an element added. The keyword "rep" in the declaration of hist 607 indicates that the Account object 605 owns the list referenced by hist, which allows the invariant 610 of Account 605 to refer to the fields of hist 607.
In the Detailed Description, we introduce the methodology in three stages, each next subsection extending the last one.
Object Invariants.
We consider an object-oriented programming language with classes. Object invariants declare constraints on values that can be stored in the fields of an object. This can be thought of as finer grained type checking, which gives even greater control of possible object field values to a programmer. In addition to invariants, programmers declare preconditions, which list states in which callers can access a specific method, and postconditions, which list states in which the method is allowed to return. Each class can declare invariants which depend on fields of the this object, as seen at 715, and on objects that are owned by the this object, as seen at 610. An object invariant specifies a relation on an object's data that the programmer intends for it to hold.
To allow a program to temporarily violate an object's invariant, each object is given an auxiliary boolean field called "inv", which specifies whether or not the invariant declared for the object holds. An object is mutable if its invariant may temporarily be violated. More formally, an object is consistent if o.inv=true. Thus, all invariants hold for consistent objects. Otherwise, the object is mutable.
In an exemplary embodiment, the inv field can be read in method contracts, that is, in pre- and post-conditions. Examples of precondition usage are shown in
The inv boolean field value can only be changed by two special statements, unpack and pack, which delineate the scope in which an object is allowed to enter a state where its invariant does not hold. Unpack sets inv to false, making the object mutable, which allows the invariants to be violated, and also allows object field assignments which might violate the invariant condition. Pack sets inv to true; but before doing so, it checks that the object invariant holds; generating an error condition if it does not.
The class IntList 705 represents an extensible list of integers. The body of IntList requires that the list elems 710 has an element added. The keyword rep in the declaration of elems 710 indicates that IntList 705 owns the list referenced by elems 710. Class IntList 705 does not refer to any fields of the elems array 710. However, ownership serves not only to protect invariants, but also to ensure that representation objects of a composite object o are accessible to a thread t after t unpacks o. That is, if elems 710 were not rep, a thread would not gain ownership of the array as a result of unpacking the IntList object 705.
The rules for maintaining object invariants are as follows:
These rules are formalized as follows, where InvT(o) stands for the invariant of class T applied to instance o.
packT o ≡ assert o ≠ null o.inv unpackT o ≡ assert o ≠ null o.inv o.f := E ≡ assert o ≠ null o.f
In this formalization, an assert statement checks the given condition and aborts program execution, if the condition does not hold.
This methodology guarantees the following program invariant for all reachable states, for each class T:
Program Invariant 0.
Accessibility modifiers (such as public and private) in contemporary object-oriented languages cannot, by themselves, guarantee that field variables consistently have only those values that the programmer intended, and are accessed only by those objects that the programmer intended. Using the methods and systems described herein confines objects and the values of the fields within much more strongly.
An aggregate is an object composed from other objects. One piece of an aggregate is known as its part or as a representation object. An aggregate owns its parts. The Account object 605 is an aggregate. Fields holding representation objects are qualified with the rep keyword. More specifically, object ownership, in one exemplary embodiment, is defined through rep fields, which establishes a hierarchy among objects; the this object owning the object referred to by the rep field, and being able to refer to any fields of the owned object. The field hist is defined as a rep field 607. This indicates that an Account object 605 owns its hist object, and can refer to the elements of the hist list.
A part is said to be leaked if it is accessible outside the aggregate. In a sequential setting, but not in a multi-threaded one—leaking is not considered harmful, as long as the parts are leaked only to be read.
Invariants are used to constrain the value space of object data fields. Invariancy and ownership are related as follows: the invariant of an object o can depend only on the fields of o and on the fields of objects reachable from o by dereferencing only rep fields. An invariant itself does not mention any quantification over objects. For example, the Account invariant 610 mentions hist, whose ownership by Account 605 is specified in the Account rep field 607. Similarly, the invariant 715 in the class IntList 705 mentions only the object elems.
To formulate ownership in such a way that invariants are not violated, each object is given an ownership field. Like inv, the owner field cannot be mentioned within the code body of a routine. An object o is free if o.owner=null. An object is considered sealed if it has non-null owner object. The ownership domain of an object o is the set collecting o and all objects that o transitively owns. The rules for pack and unpack enforce that ownership domains are packed and unpacked only according to their order in the ownership hierarchy. Furthermore, pack and unpack change the ownership of representation objects as described by the following rules, which extend the ones given earlier. The function RepFieldsT is used to denote the fields marked rep within class T.
packT o ≡
assert o ≠ null
foreach (f ∈ RepFields T where o.f ≠ null)
{ assert o.f.inv
foreach (f ∈ RepFields T where o.f ≠ null )
{ o.f.owner
unpack T o ≡
assert o ≠ null
foreach (f ∈ RepFields T where o.f ≠ null )
{ o.f.owner
With continuing reference to
Generalizing from this example, it can be observed that the methodology ensures the following program invariant, for each class T:
Program Invariant 1.
( ∀ o : T • o.inv ( ∀ f ∈ RepFieldsT , o : T • o.inv ( ∀ o : T • o.owner ≠ null
Confinement Within Threads.
An object can either be free, it can be owned by an aggregate object, or it can be owned by a thread. Correspondingly, the owner field of an object can either be null, an object, or a thread. In some languages, such as Java and C#, a thread has a representation as an object; ambiguity can be avoided in these languages by requiring that thread objects have no rep fields; thus, when a thread object appears as an owner, it denotes the thread, not the object.
Sequential reasoning techniques significantly simplify both formal and informal reasoning about program correctness. To support sequential reasoning about field accesses, a thread must have exclusive access to the fields during the execution of the program fragment to which the sequential reasoning applies. A thread must transitively own an object whenever it reads one of its fields. A thread must directly own an object to write one of the object's fields. Since no two threads can (transitively) own the same object concurrently, this guarantees exclusion.
The rules for pack and unpack enforce that ownership domains are packed and unpacked strictly according to their order in the ownership hierarchy. Furthermore, pack and unpack change the ownership of parts (representation objects) as described by the following rules:
The rules for thread ownership are as follows:
These rules give rise to the object lifecycle shown in
For an object o, if thread t packs an object p and p.ƒ=o, and ƒ is declared as a rep field 845, then the object o's ownership changes top, the object o stays consistent, but is now sealed 850. An example of this can be found in
Fully spelled out, these rules are formalized as follows, with the following comments—recall that the currently-executing thread is denoted "tid":
pack T o ≡
assert o ≠ null
foreach (f ∈ RepFields T where o.f ≠ null )
{ assert o.f.owner = tid
foreach (f ∈ RepFields T where o.f ≠ null )
{ o.f.owner
assert Legal[Inv T (o)]
unpack T o ≡
assert o ≠ null
foreach (f ∈ RepFields τ where o.f ≠ null )
{ o.f.owner
acquire o ≡
assert o ≠ null
await (o.owner = null ) { o.owner
release o ≡
assert o ≠ null
o.f:= v ≡
assert o ≠ null
x := E ≡
assert Legal[[E]] ;
In the above formalization, Legal[E] is written to denote the predicate which indicates that every object accessed in E is transitively owned by the current thread. In particular:
Legal[x] ≡ true
Legal[Eo opE1] ≡ Legal[Eo]
Legal[o.f1. ... .fn .g] ≡
o.owner = tid
o.f1.owner = o
o.f1 ... .fn .owner = o.f1. ... .fn−1
When a thread attempts to execute a statement await (P) {S}, it blocks until the condition P is true, at which point the statement S is executed; the evaluation of P that finds P to be true and the execution of S are performed as one indivisible action.
The example Bank class previously encountered in
Note that method Transfer 905 declares a postcondition 915, whereas method Transaction 930 does not. In fact, Transaction 930 cannot ensure the same postcondition as Transfer 905 as other threads might intervene between the first release 935 and the second 940, or might intervene immediately after the second release but before the calling routine resumes. For method Transfer 905, on the other hand, the postcondition 915 is stable, since the calling thread owns the account objects, which affords it exclusive access.
This methodology ensures the following program invariant, for each class T:
Program Invariant 2.
( ∀ o : T • o.inv
( ∀ f ∈ RepFieldsT , o : T •
( ∀ o : T • o.owner ∉ thread
In this section, two results are proven for the methodology. First, there are no dataraces. Second, if an object is consistent, its invariant holds.
A datarace occurs when a field is accessed concurrently by two threads and at least one of the threads is performing a write to the field. If a data race occurs, the values read or written by a thread may be unpredictable, which severely complicates reasoning about the program.
Dataraces are eliminated in this methodology by introducing redundant thread-local data into the program state, as follows:
With these modifications, the following lemma and theorem can now be proven:
LEMMA 0. The methodology guarantees that (1) holds in all reachable states.
Lemma 0 and Theorem 1 are proven together:
PROOF. Consider an arbitrary execution of the program. We prove by induction that the required properties hold in every prefix of the execution.
We look at our formalization of each program construct, as given in the previous section. Except for the unpack and acquire statement, these rules guarantee that each read or write of a field o.ƒ1 . . . .ƒn.g is protected by an expression equivalent to the expansion of Legal[o.ƒ1. . . . .ƒn.g] (we assume the evaluation of
This property is also guaranteed for the unpack statement, except for its update of o.ƒ.owner. Here, the lemma is required. By the inductive hypothesis of the lemma, we have the disjunction o.ƒ=null
For the acquire statement, the reading and writing of o.owner happens at a time when o.owner=null, as required by the theorem.
For the lemma, (1) holds in the empty prefix of the execution, since no objects are yet allocated, which means the quantifications are vacuously true. We now turn to nonempty prefixes of the execution.
Condition (1) can be violated if the quantifier's range is enlarged to a newly allocated object. But new objects are initially mutable, so (1) is maintained.
Condition (1) can be violated if an inv field is set to true, which happens only in the pack statement. There, the update of o.inv is preceded by assignments to o.ƒ.owner for representation fields o.ƒ. By the theorem, the effect of these assignments is stable, and thus, pack maintains (1).
Condition (1) can also be violated if a representation field o.ƒ is changed to a non-null value when o.inv holds. But only the field update statement writes to fields, and its update is protected by
Finally, condition (1) can be violated if p.owner is changed to a value q, when there is an object r and representation field g such that
The assignment to o.ƒ.owner in the pack statement is valid, because we argue that there are no r and g such that r.g=o.ƒ
The unpack statement changes o.ƒ.owner, so we again argue that there are no r and g such that r.g=o.ƒ
The acquire statement changes o.owner, but does so from a state where o.owner is null.
The release statement changes o.owner, but does so from a state where o.owner is a thread, not an object.
Because of Theorem 1, we no longer have to argue about race conditions. That is, in the proof of the Soundness Theorem below, we can assume values to be stable.
Consider an arbitrary execution of the program. We prove by induction that Program Invariant 2 holds in every prefix of the execution.
Program Invariant 2 holds in the empty prefix of the execution, since no objects are allocated then, which means the quantifications are vacuously true.
Consider any prefix of the execution leading to a state in which Program Invariant 2 holds. Let t be the thread that is about to execute the next atomic action. We prove by case analysis that this action maintains Program Invariant 2. In all cases, we make use of the fact that the owner field is not mentioned in invariants.
Having proved the Soundness Theorem, we can simplify the definition of Legal. In particular, we only need to check that the current thread owns the root object of an access expression and that all fields in the intermediate dereferences in the access expression are rep fields:
Legal[o.f1. ... .fn .g] ≡ o.owner = tid and f1, ..., fn are all rep fields, and for each i < n, o.f1...fi is consistent (i.e. n=0 or o is consistent).
Program invariant (1) takes care of the rest.
The soundness proof assumes an interleaving semantics. This implies that memory accesses are sequentially consistent. Sequential consistency means that there is a total order on all memory accesses, such that each read action yields the value written by the last write action.
Since Theorem (1) proves the absence of dataraces, this Soundness Theorem is relevant even in many systems with a weaker memory model, provided a happens-before edge exists between writing the owner field in the release statement and reading the owner field in the acquire statement.
Static Verification
This Soundness Theorem proves three properties that hold in every reachable state. These properties can therefore be assumed by a static program verifier at any point in the program.
By Theorem (1), we know that the values read by a thread are stable with respect to other threads. That is, as long as an object remains in the thread's ownership domain, the fields of the object are controlled exactly in the same way that fields of objects are controlled in a sequential program. Therefore, static verification proceeds as for a sequential program.
For objects outside the thread's ownership domain, stability cannot be guaranteed, as we alluded to in the discussion of the Transaction method in
When an object o enters a thread's ownership domain, we know that the invariants of all objects in o's ownership domain hold. In particular, due to our non-reentrant acquire statement and program invariant (2) of the Soundness Theorem, we have o.inv. To model the intervention of other threads between exclusive regions, a static verifier plays havoc on the fields of all objects in o's ownership domain after each acquire o operation. The static verifier can then assume o.inv. By repeated applications of program invariants (1) and (2), the verifier infers p.inv for all other objects p in the ownership domain of o. Thus, by program invariant (0), the verifier infers that the invariants of all of these objects hold.
To check our methodology at run time, we only need to check the assertions prescribed in the Confinement Within Threads section, above. However, to reason modularly about a program, as in static modular verification, method contracts should also be used. We have already seen examples of pre- and postconditions, but method contracts also need to include modifies clauses, which frame the possible effects a method can have within the thread's ownership domain.
Safe Concurrency in Java and C#
This methodology uses acquire and release as synchronization primitives. But how, if at all, does this apply to the synchronized statement of Java, or, equivalently, C#'s lock statement, neither of which explicitly include a release statement. One might think that it would suffice to map Java's synchronized statement to acquire and release statements as follows:
[[synchronized (o) { S } ]] = acquire o ; try { S } finally { release o ; }
Unfortunately, this approach is incorrect. Specifically, entering a synchronized statement is not semantically equivalent to the acquire statement because Java considers an object to be initially not owned, whereas our methodology considers an object to be initially owned by the thread that creates it. This manifests itself in the following specific behavior: in Java, the first thread that attempts to enter a synchronized statement always succeeds immediately; in our methodology, a release operation must occur on an object before any thread can successfully acquire it, even the first time, as the invariants must be set prior to the first acquisition.
Additionally, in this approach, there is no syntax for an object's initial release operation; as a result, an object could never become free. One might suggest having an implicit release operation when an object is created, and requiring even the creating thread to synchronize on the object, even in the object's constructor. But this is problematic, since it would not give the creating thread a chance to establish the object's invariant before it is released.
But there are at least two ways to achieve a correct mapping between our methodology and Java and C#. The first consists of implementing acquire and release methods on top of the language's built-in primitives. An example implementation of such acquire and release code in Java is shown in
The second way to apply our methodology to Java and C#, is by modifying the methodology. Specifically, a modified methodology exists such that executing an acquire or release statement on an object corresponds exactly with entering or exiting a synchronized statement that synchronizes on the object. The modification involves the introduction of an additional boolean field, called shared, in each object. The field is initially ƒalse, it can be mentioned only in method contracts, and it can be updated only through a special share statement.
In the modified methodology, the semantics of the statements acquire, release, and share are as follows:
acquire o ≡
assert o ≠ null
await (o.owner = null) { o.owner
release o ≡
assert o ≠ null
share o ≡
assert o ≠ null
In the modified methodology, exclusive access to an object by its creating thread during initialization is ensured not through runtime synchronization, but through constraints on the newly-introduced shared field imposed by the methodology.
Runtime Checking.
This methodology supports both static verification and run-time checking. The advantage of static verification is that it decides the correctness of the program for all possible executions, whereas run-time checking decides whether the running execution complies with the methodology. The disadvantage of static verification is that it requires method contracts, including preconditions, postconditions, and modifies clauses, whereas run-time checking does not.
If a program has been found to be correct through static verification, no run-time checks would ever fail and they can be omitted. When running a program without run-time checks, the only run-time cost imposed by our methodology is the implementation of the acquire and release statements (as in
For run-time checking, two fields, the inv field and the owner field, need to be inserted into each object. To prove race freedom, we eliminated the races on the owner fields by introducing an owns table for each thread; however, on most platforms, including Java and C#, these races are in fact benign and the owns tables can be omitted.
The computer system 1100 further comprises a thread—object consistency module 1155. The purpose of this module is to ensure that the thread table 1107 for a thread 1105 correctly records each object that the thread owns while ensuring that each owned object has an indication of which thread owns it in its owner field 1130.
An optional reader module 1160 is also included which reads an object variable field if the object is transitively owned by the thread requesting read access. A writer module 1165 is also included. This writes a value into the object variable field if the object is owned by the thread requesting write access. The system further comprises an invariant checker 1170, which ensures that the object variable field contains the invariant condition legal values, and which is called after the reader module or the writer module is accessed by a thread for a given object. If the invariant condition is found to hold illegal values, then in an exemplary embodiment an exception is thrown.
This locking methodology helps in defining leak-proof ownership domains. Several aspects of this new approach are noteworthy. First, sequentially verifiable programs are race free. Due to the necessary preconditions for reading and writing, only one thread at a time can access the objects of an ownership domain. Second, the owner of an object can change over time. In particular, an object may move between ownership domains. Third, our methodology can be efficient; it acquires only one lock per ownership domain, where the domain consists of many objects. Further, at run time, we only need to keep track of a bit per object that says whether or not there exists a thread that transitively owns the object.
Having described and illustrated the principles of our invention, it will be recognized that the various embodiments can be modified in arrangement and detail without departing from such principles. It should be understood that the programs, processes, or methods described herein are not related or limited to any particular type of computing environment, unless indicated otherwise. For example, the technologies described herein may be applied to any static or run-time program verifier.
Various types of general purpose or specialized computing environments may be used with or perform operations in accordance with the teachings described herein. Elements of embodiments shown in software may be implemented in hardware and vice versa. Various types of general-purpose or specialized computers may be used to perform the systems and methods disclosed herein. Furthermore, actions described herein can be achieved by computer-readable media comprising computer-executable instructions for performing such actions.
In view of the many possible embodiments to which the principles of our invention may be applied, it should be recognized that the detailed embodiments are illustrative only and should not be taken as limiting the scope of our invention. Rather, we claim as our invention all such embodiments as may come within the scope and spirit of the following claims and equivalents thereto.
|Cited Patent
|Filing date
|Publication date
|Nov 14, 1994
|Mar 18, 1997
|Object Technology Licensing Corp.
|Object-oriented operating system
|Jun 24, 1996
|Jan 19, 1999
|Sun Microsystems, Inc.
|System and method for space and time efficient object locking
|Sep 19, 1997
|Nov 16, 1999
|Digital Equipment Corporation
|Method and apparatus for statically analyzing a computer program for data dependencies
|Jan 13, 1998
|Feb 29, 2000
|Tandem Computers Incorporated
|Method and apparatus for translating source code from one high-level computer language to another
|Mar 5, 1998
|May 30, 2000
|International Business Machines Corporation
|System, method, and computer program product for providing an incremental storage adaptor
|Dec 19, 1997
|Jun 27, 2000
|Newmonics Inc.
|Method for efficient soft real-time execution of portable byte code computer programs
|Apr 15, 1997
|Nov 21, 2000
|Samuel C. Kendall
|Link-time and run-time error detection, and program instrumentation
|Feb 10, 1999
|Jun 4, 2002
|International Business Machines Corporation
|Method and apparatus for memory management
|Jan 21, 2000
|Aug 26, 2003
|International Business Machines Corporation
|Method and system for removing content entity object in a hierarchically structured content object stored in a database
|Jun 29, 2000
|Dec 30, 2003
|Curl Corporation
|Interface frames for threads
|Sep 21, 2000
|Aug 2, 2005
|International Business Machines Corporation
|Mutability analysis in Java
|Jan 5, 2001
|Apr 4, 2006
|Hewlett-Packard Development Company, L.P.
|System and method for verifying computer program correctness and providing recoverable execution trace information
|Mar 9, 2000
|Sep 19, 2006
|Electronic Data Systems Corporation
|Method and system for applying XML schema
|Apr 23, 2001
|Sep 26, 2006
|Electronic Data Systems Corporation
|Method and system for reporting XML data based on precomputed context and a document object model
|Dec 4, 2001
|Oct 10, 2006
|Hewlett-Packard Development Company, L.P.
|Method and apparatus for automatically inferring annotations
|Sep 30, 2003
|Jan 23, 2007
|Intel Corporation
|Method and system of permitting stack allocation to programs having open-world features
|Aug 31, 1999
|Oct 30, 2007
|Accenture Llp
|System and method for transaction services patterns in a netcentric environment
|Jan 21, 2000
|Mar 18, 2008
|International Business Machines, Corporation
|Method and system for moving content in a content object stored in a data repository
|Dec 15, 2000
|Aug 16, 2001
|Tamiya Onodera
|Method and apparatus for managing a lock for an object
|May 15, 2001
|Nov 22, 2001
|Ichiro Kyushima
|Compile method suitable for speculation mechanism
|Jan 5, 2001
|Apr 18, 2002
|Leino K. Rustan M.
|System and method for verifying computer program correctness and providing recoverable execution trace information
|Dec 4, 2001
|Aug 15, 2002
|Flanagan Cormac Andrias
|Method and apparatus for automatically inferring annotations for an extended static checker
|Oct 25, 2001
|Aug 29, 2002
|Mark Christiaens
|Topological, on-the-fly classification of objects into a global set and local sets
|Dec 4, 2001
|Sep 19, 2002
|Flanagan Cormac Andrias
|Method and apparatus for automatically inferring annotations
|Jan 7, 2002
|Jul 10, 2003
|Flanagan Cormac Andrias
|Method and apparatus for organizing warning messages
|Sep 25, 2002
|Mar 25, 2004
|Microsoft Corporation
|System and method for jointly managing dynamically generated code and data
|Sep 22, 2003
|Mar 24, 2005
|Deline Robert Anthony
|Persisted specifications of method pre-and post-conditions for static checking
|Dec 1, 2005
|Jun 29, 2006
|Hiroyasu Nishiyama
|Method for executing plural programs, method for converting source programs and compiler program using these methods
|Mar 17, 2006
|Sep 14, 2006
|The Mitre Corporation
|Semantic system for integrating software components
|Feb 7, 2006
|Oct 5, 2006
|National Instruments Corporation
|Automatic generation of application domain specific graphical programs
|Jun 8, 2006
|Oct 12, 2006
|International Business Machines Corporation
|Method, system, and computer program product to generate test instruction streams while guaranteeing loop termination
|Oct 21, 2005
|Nov 2, 2006
|Cadence Design Systems, Inc.
|Methods of model compilation
|Oct 5, 2006
|Apr 19, 2007
|Jose Iborra
|Automatic software production system
|Nov 3, 2003
|Nov 22, 2007
|Schumacher Larry L
|Execution environment for data transformation applications
|Oct 28, 2004
|Nov 27, 2008
|P.R.E-Pozitive Requirements Engineering Ltd.
|System and Method for Verifying and Testing System Requirements
|Mar 17, 1999
|May 28, 2002
|Object Technology Licensing Corp.
|Object-oriented system for the transparent translation among locales of locale-dependent application programs
|"Fugue-Protocol checking for .NET code," 1 page (downloaded from the World Wide Web on Aug. 9, 2005).
|"Fugue—Protocol checking for .NET code," 1 page (downloaded from the World Wide Web on Aug. 9, 2005).
|"Vault-a programming language for reliable systems," 47 pp. (printouts of pp. from the World Wide Web, downloaded on Aug. 9, 2005).
|"Vault—a programming language for reliable systems," 47 pp. (printouts of pp. from the World Wide Web, downloaded on Aug. 9, 2005).
|Bachmair et al., "Abstract congruence closure and specializations," Conference on Automated Deduction, CADE 2000, vol. 1831, pp. 64-78 (Jun. 2000).
|Blanchet et al., "A Static Analyzer for Large Safety-critical Software," PLDI 2003, 12 pp., Jun. 9-11, 2003.
|Burdy et al., "An Overview of JML Tools and Applications," International Journal on Software Tools for Technology Transfer, 13 pages (2005).
|C. A. R. Hoare. Monitors: An operating system structuring concept, Communications of the ACM, 17(10):549-557, Oct. 1974.
|Chandrasekhar Boyapati, Robert Lee, and Martin Rinard, "Ownership types for safe programming: Preventing data races and deadlocks," In Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, vol. 37, No. 11 in SIGPLAN Notices, pp. 211-230, ACM, Nov. 2002.
|Chang et al., "Abstract Interpretation with Alien Expressions and Heap Structures," Technical Report MSR-TR-2004-115, 27 pp. (Jan. 2005).
|Chang et al., "Inferring Object Invariants," AIOOL, 11 pages, 2005.
|Cormac Flanagan and Stephen N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proceedings of the 2004ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), vol. 39, No. 1 in SIGPLAN Notices, pp. 256-267, ACM, Jan. 2004.
|Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), vol. 37, No. 5 in SIGPLAN Notices, pp. 234-245, ACM, May 2002.
|Cousot et al., "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints," Conf. Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238-252 (Jan. 1977).
|Cousot et al., "Automatic discovery of linear restraints among variables of a program," Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84-96 (Jan. 1978).
|Cousot et al., "Systematic design of program analysis frameworks," Sixth POPL, pp. 269-282 (Jan. 1979).
|Das, "Unification-based Pointer Analysis with Directional Assignments," PLDI 2000, pp. 35-46.
|David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe, "Extended static checking," Research Report 159, Compaq Systems Research Center, Dec. 1998.
|DeLine et al., "Typestates for Objects," Proc. European Symp. on Object Oriented Programming, 26 pp. (2004).
|Deutsch, "Static Verification of Dynamic Properties," Polyspace Technologies, Inc., 8 pp. (Nov. 2003).
|Doug Lea, "Concurrent Programming in Java," Addison Wesley, 2000.
|Erikß Abrahßm-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. "Verification for Java's reentrant multithreading concept," In Foundations of Software Science and Computation Structures, 5th International Conference, FoSSaCS 2002, vol. 2303 of Lecture Notes in Computer Science, pp. 5-20, Springer, Apr. 2002.
|Fahndrich et al., "Adoption and Focus: Practical Linear Types for Imperative Programming," 11 pp. (2002).
|Gulwani et al., "Join algorithms for the theory of uninterpreted functions," Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science, 12 pp. (Dec. 2004).
|Hoare et al., "An axiomatic definition of the programming language PASCAL," Acta Informatica, vol. 2, No. 4, pp. 335-355 (1973).
|Hote et al., "Run-Time Error Detection through Semantic Analysis: A Breakthrough Solution to Today's Software Testing Inadequacies," Polyspace Technologies, Inc., 10 pp. (Sep. 2001).
|Hudak et al., Collecting Interpretations of Expressions, ACM, ACM Transactions on Programming Languages and Systems, vol. 13, No. 2, pp. 269-290, Apr. 1991.
|James Noble, Jan Vitek, and John Potter, "Flexible alias protection," In Eric Jul, editor, ECOOP'98-Object-oriented Programming: 12th European Conference, vol. 1445 of Lecture Notes in Computer Science, pp. 158-185, Springer, Jul. 1998.
|James Noble, Jan Vitek, and John Potter, "Flexible alias protection," In Eric Jul, editor, ECOOP'98—Object-oriented Programming: 12th European Conference, vol. 1445 of Lecture Notes in Computer Science, pp. 158-185, Springer, Jul. 1998.
|Jeremy Manson and William Pugh, "Requirements for programming language memory models," Workshop on Concurrency and Synchronization in Java Programs, in association with PODC, Jul. 2004.
|Jones et al., "Flow analysis and optimization of Lisp-like structures," in Program Flow Analysis: Theory and Applications, Ch. 4, pp. 102-131 (1981).
|K. Rustan M. Leino and Peter M³ller, "Modular verification of global module invariants in object-oriented programs," Technical Report 459, ETH Z³rich, 2004.
|K. Rustan M. Leino and Peter M³ller, "Object invariants in dynamic contexts," In Martin Odersky, editor, European Conference on Object-Oriented Programming (ECOOP), vol. 3086 of Lecture Notes in Computer Science, pp. 491-516, Springer-Verlag, 2004.
|Lahiri, S. K., "Unbounded System Verification Using Decision Procedure and Predicate Abstraction," Ph.D. thesis, Carnegie Mellon University, 273 pp. (Sep. 2004).
|Leino, "Toward Reliable Modular Programs," Ph.D. Thesis, California Institute of Technology, 183 pp. (1995) (available as Technical Report Caltech-CS-TR-95-03).
|Lev-Ami et al., "Putting static analysis to work for verification: A case study," International Symposium on Software Testing and Analysis, pp. 26-38 (2000).
|Logozzo, "Separate compositional analysis of class-based object-oriented languages," Proc. of the 10th Int'l Conf. on Algebraic Methodology and Software Technology, vol. 3116, pp. 332-346 (Jul. 2004).
|Logozzo, F., "Class-level Modular Analysis for Object Oriented Languages," SAS 2003, pp. 37-54.
|McCarthy et al., "Correctness of a compiler for arithmetic expressions," Proceedings of Symposia in Applied Mathematics, 11 pp. (1967).
|Meyer, B., "Object-oriented Software Construction," Series in Computer Science, Prentice-Hall International, 82 pp., 1988.
|Mike Barnett and David Naumann, "Friends need a bit more: Maintaining invariants over shared state," In Dexter Kozen, editor, Mathematics of Program Construction, Lecture Notes in Computer Science, pp. 54-84, Springer, Jul. 2004.
|Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte, "The Spec# programming system: An overview," In Construction and Analysis of Safe, Secure and Interoperable Start devices (CASSIS), Lecture Notes in Computer Science, Springer, 2004.
|Mike Barnett, Robert DeLine, Manuel Fõhndrich, K. Rustan M. Leino, and Wolfram Schulte, "Verification of object-oriented programs with invariants," Journal of Object Technology, 3(6):27-56, 2004.
|Nelson et al., "Simplification by cooperating decision procedures," Stanford Artificial Intelligence Laboratory Memo AIM-3 11, 21 pp. (Apr. 1978).
|Nelson, "A generalization of Dijkstra's calculus," ACM Trans. on Programming Languages and Systems, vol. 11, No. 4, pp. 517-561 (Oct. 1989).
|Peter M³ller, "Modular Specification and Verification of Object-Oriented Programs," vol. 2262 of Lecture Notes in Computer Science. Springer-Verlag, Oct. 8, 2001. PhD thesis, FernUniversitõt Hagen.
|Poetzsch-Heffter, "Specification and verification of object-oriented programs," Habilitationsschrift, Technische Universitõt M³nchen, 162 pp. (1997).
|Robert DeLine and Manuel Fõhndrich, "Enforcing high-level protocols in low-level software," In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), vol. 36, No. 5 in SIGPLAN Notices, pp. 59-69, ACM, Jun. 2001.
|S. S. Owicki and D. Gries, "An axiomatic proof technique for parallel programs," Acta Informatica, 6:319-340, 1976.
|Sagiv et al., "Parametric shape analysis via 3-valued logic," ACM Transactions on Programming Languages and Systems, vol. 24, No. 3, pp. 217-298 (2002).
|Shaz Qadeer, Sriram K. Rajamani, and Jakob Rehof, "Summarizing procedures in concurrent programs," In Proceedings of the 2004 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), vol. 39, No. 1 in SIGPLAN Notices, pp. 245-255, ACM, Jan. 2004.
|Steensgaard, B., "Points-to Analysis in Almost Linear Time," 23rd POPL (1995), pp. 1-10.
|Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas E. Anderson, "Eraser: A dynamic data race detector for multi-threaded programs," ACM Transactions on Computer Systems, 15(4):391-411, Nov. 1997, Also appears in Proceedings of the Sixteenth ACM Symposium on Operating System Principles, pp. 27-37, Operating System Review 31(5), 1997.
|Stephen N. Freund and Shaz Qadeer. Checking concise specifications for multithreaded software, Journal of Object Technology, 3(6):81-101, Jun. 2004.
|Stransky, "A lattice for abstract interpretation of dynamic (LISP-like) structures," Inf. Comput., vol. 101, No. 1, pp. 70-102 (1992).
|Venet et al., "Precise and Efficient Static Array Bound Checking for Large Embedded C Programs," PLDI 2004, pp. 231-242.
|Yi et al., "Automatic generation and management of interprocedural program analyses," ACM, pp. 246-259, 1993.
|Citing Patent
|Filing date
|Publication date
|Aug 27, 2007
|Sep 11, 2012
|International Business Machines Corporation
|Lock reservation using cooperative multithreading and lightweight single reader reserved locks
|Apr 13, 2011
|Feb 25, 2014
|International Business Machines Corporation
|Impact indication of thread-specific events in a non-stop debugging environment
|Apr 13, 2011
|Apr 15, 2014
|International Business Machines Corporation
|Event management in a non-stop debugging environment
|Dec 3, 2012
|Apr 15, 2014
|International Business Machines Corporation
|Event management in a non-stop debugging environment
|Feb 24, 2011
|Jun 10, 2014
|International Business Machines Corporation
|Thread-specific event management in a non-stop debugging environment
|Dec 4, 2012
|Jun 17, 2014
|International Business Machines Corporation
|Impact indication of thread-specific events in a non-stop debugging environment
|Nov 12, 2012
|Jun 17, 2014
|International Business Machines Corporation
|Thread-specific event management in a non-stop debugging environment
|Feb 16, 2011
|Jun 24, 2014
|International Business Machines Corporation
|Event management in a non-stop debugging environment
|Nov 12, 2012
|Jun 24, 2014
|International Business Machines Corporation
|Event management in a non-stop debugging environment
|Apr 6, 2012
|Aug 19, 2014
|Hwlett-Packard Development Company, L. P.
|Identifying globally consistent states in a multithreaded program
|Dec 27, 2013
|Oct 4, 2016
|Sunedison Semiconductor Limited
|Methods and systems for deterministic and multithreaded script objects and script engine
|Aug 27, 2007
|Mar 5, 2009
|International Business Machines Corporation
|Lock reservation using cooperative multithreading and lightweight single reader reserved locks
|Feb 24, 2011
|Aug 30, 2012
|International Business Machines Corporation
|Thread-Specific Event Management In A Non-Stop Debugging Environment
|Dec 27, 2013
|Aug 7, 2014
|Sunedison, Inc.
|Methods and systems for deterministic and multithreaded script objects and script engine
|U.S. Classification
|718/107, 717/116, 719/316
|International Classification
|Cooperative Classification
|European Classification
|Mar 10, 2005
Owner name: MICROSOFT CORPORATION, WASHINGTON
Free format text: ASSIGNMENT OF ASSIGNORS INTEREST;ASSIGNORS:LEINO, K. RUSTAN M.;SCHULTE, WOLFRAM;JACOBS, BART;REEL/FRAME:015760/0076;SIGNING DATES FROM 20050212 TO 20050302
Owner name: MICROSOFT CORPORATION, WASHINGTON
Free format text: ASSIGNMENT OF ASSIGNORS INTEREST;ASSIGNORS:LEINO, K. RUSTAN M.;SCHULTE, WOLFRAM;JACOBS, BART;SIGNING DATES FROM 20050212 TO 20050302;REEL/FRAME:015760/0076
|Jan 28, 2014
|Fee payment
Year of fee payment: 4
|Dec 9, 2014
Owner name: MICROSOFT TECHNOLOGY LICENSING, LLC, WASHINGTON
Free format text: ASSIGNMENT OF ASSIGNORS INTEREST;ASSIGNOR:MICROSOFT CORPORATION;REEL/FRAME:034543/0001
Effective date: 20141014


text:
This is a small restaurant tucked away in a side street near the market square (there is a weekly market on Saturdays). It is very like a family home, not just atmosphere, decoration and food, also the patrons, which are almost all locals. One table seems to be reseved for a group of men in their seventies (or older) which... More
Add Photo

subset: commoncrawl


text:
Team BlackSheep Vendetta LED Cover
Team BlackSheep
$1.99 Flat Rate Shipping!
|Low Price:
This item is eligible for $1.99 flat rate shipping Learn More
This item earns up to 2 VIP Reward Points Learn More
A replacement LED cover for the TBS Vendetta.
This product was added to our catalog on June 6, 2016.


text:
"Garments create the person" truly means "like gown, like character." Appearance are near to eachother as are garments to the skin of 1. Garments possess an essential and unique mental impact on the person. While fig leaves where the character traits exposed were the then-new emotions of shame and modesty. Since that time, however, garments have grown to be individual feelings more complicated and more sophisticated. Nowadays character is exposed in all in that which you fabrication de vetement femme possess as well as you do. Your garments are no exception. They, also, expose that which you are even periodically that which you are organizing and considering. They provide hints for your psychological growth, your character, as well as your level of readiness.Garments are an easy method of self expression. They're the individuals self-image image's external symptom. They're just one area of the self image, simply because they give the planet a photo they've organized from the choice of their garments however they are an essential component.
Garments show your psychological reactions as well as your mental heat alive. They provide a hint regarding that which you are experiencing about issues and how. They provide a mental account of the character.Psychological uncertainty can also be proven in sporting high-fashion garments that are unsuitable or cozy. People who use apparel that is such might have low-self- confidence and never trust their particular view.Negligence in gown is characteristic of contempt toward establishments, cultural traditions, and others. Folks who are intentionally unkempt understand that people may discover them-and oftentimes that is welcomed by them. Culture is being told by them how they experience it. "you can observe how personally I think about your silly regulations as well as you and conferences. I'm that above all!"
Garments are an essential area of the capability to not be unhappy. Those who have a smart attitude toward garments possess a smart attitude toward living. Being together with your garments at ease means being with your personal character at ease.Suggestion on apparel: brown is worn by Researchers! Need evidence of apparel exposing character? Visit a location where you are able to notice cultural workers, researchers or advisors. The most of them is likely to wear brown and "planet" shades.Today visit a location where you are able to notice doctors or lawyers and take notice of the predominance of charcoal or dark with scarves. These are energy garments.


text:
Start a Trial
Sign in
Historical Events
Family Trees
Become a Member
Become a Member
New Braunfels Herald Zeitung Newspaper Archives
March 08, 1994
- Page 1
First Name
Last Name
With All of the Words
With the Exact Phrase
Go to advanced search
Discover Your History
Issue Date:
Tuesday, March 8, 1994
Pages Available:
Previous Edition:
Sunday, March 6, 1994
Next Edition:
Wednesday, March 9, 1994
New Braunfels Herald Zeitung
Publication Name:
New Braunfels Herald Zeitung
New Braunfels, Texas
Pages Available:
Years Available:
1952 - 2013
Learn More About This Publication
2.17+ Billion Articles and Growing Everyday!
More Than 400 Years of Papers. From 1607 to Today!
Articles Covering 50 U.S.States + 22 Other Countries
Powerful, Time Saving Search Features!
Find Your Ancestors Now
Newspaper Archives
Birth Records
Census Records
Marriage Records
Death Records
Divorce Records
Military Records
View Sample Pages : New Braunfels Herald Zeitung, March 08, 1994
Page 2
Page 3
Page 4
Page 5
Page 6
Page 7
Page 8
Page 9
Page 10
Get Access to These Newspapers
Plus 2.17+ Billion Other Articles
NewspaperARCHIVE.com -
Used by the World's Finest Libraries and Institutions
OCR Text
New Braunfels Herald Zeitung (Newspaper) - March 8, 1994, New Braunfels, Texas M016 10/22/99 196 SO-WE SI rn rCROPUBLI SH J NG 2627 E YANDELL DR EL PASO, TX 79903- TUESDAYStatewide voter turn out expected to be light today - See Page 2 SCENTS OOUNTDOWNi 382 DAYS NswBriunWi OttQuiotnlviniii Mvch21.1846 Mwch21.1M6 New BravuifelsHerald'Zeitung UW4_SwvlnQConnlCounlytof mowttwn KavtiW How ot TOMMY OWIg ■VbL142,Na83 Inslcie CX)ltusrlsi.......................................2 Wtitfwi/WflsrWMol^ count ..2 CroMKVord......................................3 Oplnton..........................................4 Sport! Diy«..................................7,8 Th# Mirkstplsot.......................0.10 SlLininilisclv BlrllMlay wMim Iroiii th> Hwld 8»Hinl New Bnauftls Herald-Zctosif exmls the foOowiiig biftlidiy wiAei to; Tommy Ortk^ Rome Brbem, Robert Coker, LommLemmoneCfheyeent), Damay Yberra, OtetmMaek, Sr^ (50yoaref),Mlke Webek (kelak rtOfBrlea Renee Leat 0yeanl), Anke Leat Riot, Cowboys T^ohlfto now •valloblootH-Z CommemontiveDtllu Cowboy! T-ihiits are now ivsiltbte through the New Braunfels Her-aid-Zettung. Cuitomen wishing to Older these unique ihixtB iMydoioby pla^onleikvC] TOTLsndtSt VT Customers should lUow seven buiinew days fbr delivenf. Ply-bent required upon ofdering. * All sizes ire tviilible, including youth sizes end luge iduhs SiZCT. For mole infoonslioo, call Advtfdsiqg Director Piul Davis al 625-9144. Marschund Wondorgnippo to moot March 18 The Msisch und Wsndeigiuppe will meet TXiesdsy, Match IS, et the Senior Citizens Centei; 655 Lands St Social time is 7 p JU. with the meeting following a 7*J0. Bfoaotioo8lnti gypport group adiMlHtod to ■uuams aet sisrevs resreiwii ire The New BnunMs Breastfeeding Support OiDup will meet on 1\ieadsy, March 15, a IO un. a the New Braunfels Presbyterian Church. All breastfeeding moms and moms4o-be are invited to attend. For more informstioo, oootart Data a 625-1240 or Stephanie a 620-1545. MB yeah Woo prooiam o^iodulod h*8 Springdme!!! So have a blart and sp^ an afternoon in the park inaking and flying kites S^[MoiSo^B^taea's *Tfeture*sWqf:Upb Upland Away!** The program is ibr anyone age 6to 15 years old. It will take place TViead^f, Match 22,1994, ftomdpittDd pJU. a Prince Solma Park. The fee is $4 per pencil. Pte-regiaDation is required and will be taken until March 21,1994, athe parks oflioe Monday to Friday a I IO Golf Course Road. * For more infbimatioo call (?10) 608-2160 or come by the parb oOloe. (TheNewBram^U Herald-ZeiiuniinvtieeUtreadertioeiib-wititemtmStamdeek \AceordtnitotheSoplimibart I Anklet and membert of the OermmcommMnUy, ''SmmedeehrrepruenuaeUdni \plaeefi)r members (fthe eonrnm-\nliy so gather and share the day's \heg>peninMS,Weim4seyoulo Ishmeydtkns,) Two dead after murder/suidde Man turns gun on himself when police ask him to get out of car ByJBHiPBflVIOIilPEL Staff Writer Comal County SherifTa deputies an itiveaigadng • murden^cida flat is reported to have occurred early 1\iesday morning a Cation Lake. Officials saki T^idnda Hines, 35, of Cation Lake, was shot in the head and WU dead a the scene. David Hines, 39, of Mission, was also shot in the head. He was transported to McKenna Memorial Hospital after the inddea and died a 6 am today. Accoiding to CCSC offidals, the incident occurred a 3:30 am l\iea-day. Deputies received a call reporting a shooting a 529 Flintaone Drive in the Mobile Home Estates aubdiviaion on the south side of the lake. The caner reported tha the sssaflsit. David Hines, had fled in the victim's car. Offidals said Deputy Tim Nowell was responding to the call when he HMdlMwv photo by JOHN HUSETH Comal Counlv SherifTa daoiitles look for evlrtence aoon after an anoaranl OfHdala aald they ranov- ared a 0 mm Huger Inalda tha car. observed the car; a 1986 Subaru statioo Hoherz, tire deputy pursued the car on The vehicle was stopped one half wagon, passing him. Farm to Market Road 306 toward mile east of Purgatory Road. Aoonding to Chief Deputy Bwood Interstate Highway 35. **He got out of his car and krrew he 'N* got out of his ami laww Im hud a pe» sMrt MrtrtUwila Mrt aakad him to out of Ms osfo' -CNgf Deputy BwoodHohari had a possible aaaailant He asked Urn to step out of his car,** said Hoherz. Hoherz said David Hines did not get out of the car even after the deputy had commanded him two more times toeidtthevehide. It sppeara the man put a gun to his head and shot hirnseli; aoconling to HohecL Reports show NoweD had his Ughrt shining irto the car. Deputies recovered a 9 mm Ruger semirtitomatic weapon in tire car and ftjund several spent shells in tire car and the house. Lucinda Hines* 13-year-old daughter observed the shootfeg at tire home. Offidals said tire couple had recendv gottoi a divorce. Lucinda Hines* death was ruled a murder by histioe of tire Peace Howard **Curly** Smith. Officials are waiting ballistics tests befbre ruling on David Hines* death. Deputies are continuing to investigate fee case. Investigaton on tire case are Detective Jimmy Ummer and SgL David Ort. Officio identify fywith Hill girFsl help from news /M^ZrtWV photo by JOHN HUSETH Car catchns fire on 1-35 A Ma modal BuWc Ragal caught fire on the northbound lane of 1-39 north of tha Oonrada/Kohlinhorg axil yea-tarday momlna al appraxMialaly 7:30 am No Injuriea were reported from the fire, but the Inddent caused the oloalnn oilha aiiarataie fOr IO mkiulan Maw Rr«**nfela Flrt nsnirmsnt narannnal raannrnlail tn tha rail anrt axllngulahad tha fire wkhln a law mfrMJlirt ByJBMFERROMPEL Staff Writar Comal County Sheriffs deputies have identified tire body of t girl fijund on North Cranes Min Road more than one year ago. Tte girl WU identified u Emily Jeanette Qaida, 15, of San Antonio. Reports show her body WU fbund by Comal County road crews on Feb. 25, 1993. She had been sexually asaauhed and strangled, according to part reports. The girl WU identifled afler a newscast WU aired on San Antonio television station KSAT Channel 12. Hie report WU broadcast on tire tnnive^ ssi^ dale of the discovery of the Otf-da*s body» According to CCSC officials, the girl's mother wu living out of state and hid recently returned to San Anto nio. A friend of Garda's mother sur tire newscast and told her to call tire Comal County Sheriff's Office. Chief Deputy Elwood Hoherz, of tire Comal County Sheriffs Office, said the mother had been looking fiv her daughter for more than a yeu. Garcia was positively identified because she had been fingerprinted when she WU a child. ** We were able to UU thou to make a positive idenriflcrtion,** arid Hohen. Deputes are now conducting fliflier investigrtion into tire murder. Several leads have been provided but no inert is expected soon, icooiriiQg to Hoheo. **We think it may be gang relaied. We have several namu to proceed on,** he said. Garcia wu three to fbur months pregnant when she wu found. Her mother said she had left home in January 1993, according to Hoherz. $87.8 million spent in restaurants last year, figures up by 7 percent From Staff Rsports The New Braunfels Chapter of the Texas Restaurant Aaaoclation announced this week that New Braunftda leaidetzs ppent $87.8 mil-lion in area lertaurants during 1993, an incBBsu of 7.12 percent over 1992 levels. Mexican lertauiants sell the No. I fttodpmchaaed by New Braunfels ootiaurnen^ wife leridenli mending a total of SI 1.6 million or 14.^ pere^ of their raatauraflt doHan. Hamburger reatauiinta tout the aeoond mort popular fbod In New Braunfels, accounting fbr nearly capture 10A3 paioeDtof lertauiart exp^-turea. OvenU, New Baunfth ooBaumea apaid 17.9 miUioQ per year co aloo-hoUo beverages in ana reatauiarts. Rapoita alto show that New Braunftsla restaurants oootributed 16.6 million to atata and local tax coffers during 1993. New Braunfels neoeivedSl.l millioo finn their share of restaurant rtlu Ox nwenueA while collecting $273/X)0 for their ahare of mixed beverage tax revenues, bringing total tax revemrea of SIJ milliootDthearBa. *1t is difficult to deiennine the true Ox oootiibutioo of our city's restau-nnts because ifs impoaaible to identify tha value of property taxes, pe^ mlt feu and otfau rex revemres. But WB are pleased to be part of an industry that oontributu so much to city revenues,** said Robert Konkel, piea-ident of the New Braunfels Rutau-lant Aaaodation. Reitaurants also stimulata the economy by creating Jobs fbr 2,684 retideots wife wagu in exceu of $21.9 millioo annually. Tha 1993-94 Texu Restaurant Aaaodation PresidBnt David Cortez will speak at 6:30 p.m. March IO at the PUrts Diner rt 367 Main Plea in New Braunfels. For infbcmation contact Konkal at (210)625-2954. CISD trustees approve purchase of seven portable buildings, renovations Board also approves program which will place uniformed officers at Smithson Valley By ROW MARK EASH Stdfy^ffitor The Comal Independent Schod District board of tniateu have approved $1,064,000 in expendituru to addrca space tequirenrents fbr the 1994-1995 school year. All except $100^000; which had previously been approved fbr warehouring fhdlities, was approved unanimously at Monday nlgfaf a board merting. The diitict will purchau seven portable building, endoae tire outdoor gymnasium it Bill Brown Elementary and renovate a portion of the old Canyon Middle School wife the funds. The portable buildings are estimated rt $50,000 each fbr a total of $350,000. Endoring the gymnarium at Bill Brown is estimated at $14,000 and the eatimrtB fbr renovadrrt the old Canyon Middle School to pcovidB cafeteria servicu and fbur addition-a1 claaiiooiiis is estimated rt $614,000. I Acooiriing to Abel Campos, Financial Dfrector fbr CISD, the funds are available from various louxoaa. **We have $450,000 fe the budget from tha three Ocilla on our tax rata fbr thii type of rtuff,^ Mid Campos. **Thi state bu also granted us a portion of our appeal ftir fundi that were not in their estimated revenuu fbr us becaure of incieiaed enfoUment Thrt riiouki ba about $500,000. The diflbenoe will come out of our fund balance which last year was $5 miUion.** Campos added, however, thrt borrowing from tire fUnd balance rrreana thrt additional fundi will have to be borrowed in the fall to start the school year. The fund balance is used to offhet the amount borrowed each year. In other buafeeaa tire board also rtiproved a leioludon and security implementation with tire Alamo Area Narootics Trek Force. Seventy-five percent of tire coal of this pilot program will come from grant monies, however, tire district will pay the other 25 percent—$25,000. The program will place unifbnned officers on tire cam-puaes of SmlfeacMi Valley High School and Smithson Val-layMiddla School. Tha next board meetirre will take plaoe on March 24 at 7:30 p.nLrtSinifeionViiUey High School, 4001 Hwy. 46 Wert in Smitbren Valley.Don't miss Horizons '94 - Coming March 27 in the Herald-Zeitung! ;
About Us
Contact Us
Free Newspaper Archives
© Copyright 2017 NewspaperARCHIVE.com. All rights reserved.


text:
No products
Check out
Product successfully added to your shopping cart
Display all pictures
Model 132
280,00 € Tax incl 231,40 € Tax exc
Out of stock
Add to cart
This product is not sold individually. You must select at least 1 quantity for this product.
Have Questions? Ask about this product.
Be the first to write your review !
Brocha de Afeitar Tejón Punta Plata Marfin Joe Black
* Required fields
Send Cancel


text:
Davao City, Philippines [ show map ]
I'm here to meet guys from 25 to 60 years old for dating, friendship and serious relationship.
A sweet, caring and funny person .. I love what i am doing specially those things that are interesting.
i am looking for someone who can give happiness, acceptance and loving me unconditionally..


text:
The casual observer at the city's waterline can easily pick out swooping sea gulls and a fish-faced pelican or two. But would you know an oystercatcher from a double-crested cormorant? You will if you attend "Birds of the San Francisco Coast," a free, expert-led nature walk that winds through Lincoln Park and Land's End in search of feathery friends. The easy 1-1/2-hour hike begins at 10 a.m. at the Coast Trail trailhead in Lincoln Park, at the large parking lot at the end of El Camino del Mar (off Point Lobos), S.F. Call 621-3260 or visit www.sfneighborhoodparks.org.
-- Joyce Slaton
Salty Sport
Yachts on the loose
Don't you miss the good old days of the Reagan era, when pink and green clothes were all the rage? When Sperry Top-Siders were worn with pride, and you and Mimsy would traipse to Newport for a leisurely day on the S.S. Wasp?
Come relive your preppy youth with a day of dry martinis and sweaters tied around the neck at the Il Moro Trophy, the second race of the annual Bay Area Challenge Series. Six restored America's Cup-class boats duke it out on the briny for nautical supremacy, starting at Angel Island and winding through the bay to Sausalito. Katharine Hepburn would have thought it very "yar." The ships set sail at 10 a.m. daily. Viewing areas in San Francisco include the northern end of the Embarcadero and the eastern end of the Presidio. Admission is free; call 289-0401 or visit www.challenge-series.com.
-- Kevin Chanel
Up and At 'Em
It's the best place to see flying elephants outside of a Dumbo screening -- the Berkeley Kite Festival and West Coast Kite Championships are on again, as flyers from around the world descend on the Bay Area for a weekend of sky-borne silk and color. Oooh and ahhh at aerial ballets involving Japanese-style kite battles, kite-powered buggies, and a world-record attempt for the longest stack of kites ever flown. There will also be 20,000 square feet of giant fabric creatures, including geckos, pandas, and, yes, elephants. Kids can try free kite-making and -flying lessons; adults who just wish they were kids can try out the latest advanced designs and go shopping in the giant sales tent. The festival starts at 11 a.m. both days at Cesar E. Chavez Park at the Berkeley Marina, Marina & Spinnaker. Admission is free; call (510) 235-5483 or visit www.highlinekites.com. -- Jack Karp


text:
Home > Wheat Free Recipes > Raspberry Thumbprint Cookies
Raspberry Thumbprint Cookies
Wheat Free Recipe
Raspberry Thumbprint Cookies contain crushed walnuts and brown rice flour for healthy and nutty treats. Fruit sweetener sweetens these pretty raspberry cookies.
1-1/2 cup walnuts
1-1/4 cup butter
5/8 cup fruit sweetener
3 egg yolks
1-1/4 teaspoon vanilla extract
2-1/2 cups brown rice flour
1/2 teaspoon salt
3 egg whites
3/4 cup low sugar raspberry jam
Recipe Directions
Preheat the oven to 350 degrees. Toast the walnuts in the preheated oven for 7-10 minutes, stirring occasionally. Let the nuts cool, then process in a food processor, using a pulsing action, until they are finely ground. Do not over-process or you will end up with a paste.
Cream together the butter and fruit sweetener until light and fluffy. Add the egg yolks one at a time, beating well between each addition. Stir in the vanilla, flour and salt. Cover the dough and refrigerate for 20 minutes to make it easier to handle.
Preheat the oven to 350 degrees. Line baking sheets with baking paper. Use a number 24 scoop (2 tablespoons) or a spoon to scoop out the dough and form in into balls.
In a small bowl, stir the egg whites with a fork just to break them down. Roll the cookie balls in the egg whites. Then drain the cookies and roll them in the ground walnuts.
Place the cookie balls 2 inches apart on the prepared baking pans. Flatten each ball to 1/3 inch thickness. Then press a thumbprint in the center of each cookie.
Fill each indentation with 1 teaspoon of raspberry jam. Bake the cookies in the preheated oven on an insulated or double pan for 15-18 minutes, until the cookies are golden around their edges. Let the cookies cool completely on the pans before removing them. As these are especially fragile when they are warm, handle them with care.
Yield: 3 Dozen
Baking Tip
To make uniform impressions in delicate thumbprint cookies, wash the outside of a small extract bottle. Press the bottle with the cap in place into the cookies and twist for nice deep indentations. Fill them as directed.
You may also like...
Wheat Free Tip
Wheat free snack idea: Raw nuts and seeds, or flavored with tamari.


text:
Hotels in Sidney, Victoria
Search Sidney Hotels
Get Secret Prices on selected hotels
These prices aren't available to everyone.
View hotels in Sidney on a map
- Royal Jubilee Hospital
- Butchart Gardens
- Victoria Bug Zoo
- University of Victoria
- Government Street
- Abkhazi Garden
- Save-On-Foods Memorial Centre
- British Columbia Parliament Building
- Bear Mountain Golf and Country Club
- Victoria Conference Centre
- Bear Mountain Golf Club
- Royal BC Museum
- Royal Roads University
- Esquimalt Lagoon Migratory Bird Sanctuary
- Cordova Bay Golf Course
- Camosun College - Interurban Campus
- The McPherson Playhouse
- Hatley Castle
- Victoria Royal Theatre
- Uptown Center
Best Cheap Sidney, Victoria Hotels
Hotels in Sidney
Hotels in Sidney mostly cover the mid segment of the market but there is a range of hotels suitable to most travelers, including couples, families, and solo travelers. The popular Sidney Pier Hotel and Spa is a 3-star hotel in Sidney featuring modern décor and providing guests with spacious rooms right on the centrally-located Sidney Pier. The hotel houses a spa and fitness center, as well as a library for relaxation. Meanwhile, the By the Sea BnB in Sidney has a welcoming environment where guests will no doubt feel at home. The hotel offers a splendid garden to relax in, and a central and convenient location.
Things to see in Sidney
For a fun day out for all the family, the Shaw Ocean Discovery Center on Sidney Pier is home to all sorts of sea creatures that will amaze everyone. Not to be missed are the touch pools where you can pet some of the waters' weirdest animals. The Sidney Spit Marine Park is also an ideal spot for enjoying nature but in a more tranquil environment. For aviation enthusiasts, Sidney reviews recommend the British Columbia Aviation Museum. Located on the edge of the airport, this lovely museum is maintained by a team of committed and friendly staff. Staying with the theme of history, Sidney Museum and Archives is a wonderful little museum with both permanent and temporary exhibitions on the neighborhood's past. After all that, you might be feeling a little hungry, so head to Roger's Chocolates, a popular little shop selling some very tasty treats.
Good for families
With plenty to keep both kids and adults busy, Sidney is the ideal Victoria neighborhood for families. Located away from the hustle and bustle of the downtown, this neighborhood offers plenty of family-friendly activities, such as the Shaw Ocean Discovery Centre and the Aviation Museum. Families can also head out on the water to go dolphin and whale watching; the sight of these magnificent and graceful beasts is sure to fascinate and inspire both young and old. Plus, the neighborhood offers watersports, including snorkeling, and kayaking. And for accommodation, hotels in Sidney offer great rates that will suit most families' budgets.
How to get to Sidney
Visitors can travel to Victoria International Airport from across Canada and various major cities in the United States. Layovers in Toronto and other North American cities are available if you are traveling from further afield. Sidney is just a stone's throw away from the airport: travelers can reach the neighborhood on bus services operated by BC Transit. Just take service 83 or 88 direct to the neighborhood. Various taxi companies also operate services between the airport and Sidney. Once here, travel in Sidney is simple: visitors can walk or drive to many places, while public buses are also available.
Things To Do in Sidney - Victoria Travel Guides
Where to Stay in Victoria - Waterfront Hotels, Family-Friendly Motels, and Heritage Homes
Victoria is brimming with places to stay, whatever your taste and budget. You can go for a waterfron...
Victoria Shopping Guide - From Independent Boutiques and Bookstores to Produce Markets and Fashion Malls
Shopping in Victoria can mean popping in and out of indie boutiques or visiting a market and stockin...
Victoria Attractions - Discovering the City's Harbor, Heritage, and Natural Beauty
When you visit Victoria, you can explore grand Edwardian architecture or kayak past floating homes a...


text:
Call now! 866 306 5727
Cash For scrap cars Mattapoisett Massachusets is the scrap car removal service in Mattapoisett Massachusets that turns your cars into money as fast as asap The reliable money for scrap car Mattapoisett MA is ready to help you get rid of the junk cars in Mattapoisett MA. Do you need to make some fast money as soon as possible? Recycle your scrap cars and help the earth! money for scrap car Mattapoisett Massachusets is the best way to get fast money and your cars disposal at same time. The tow truck will give you a money, a receipt in Mattapoisett Massachusets and take your cars a way to a scrapyard closed to Mattapoisett Massachusets where It will be properly disposal. You do not pay us but instead we take your junk cars in Mattapoisett MA and paid you money on the spot. You can reach us by phone or website form to schedule the best time in Mattapoisett Massachusets that works for you.
You shouldn't hold off any longer, but instead make the call right now,scrap cars removal Mattapoisett MA, Our professional workers know how to Tow your junk car away the property in Mattapoisett MA. If your cars has completely damaged or broken down and you can't pay big fee to repair it then give us a call and we will pay cash and remove your scrap cars as soon as possible. Our mission is to provide fast, hassle free service as well as best customers service in every step of the way. Our experts will help you in your plan of get rid of you crap cars in Mattapoisett MA asap. If you need to get cash for any cars, van, or trucks then it isn't easy as you feel! Call us and get your cash Fast. Cash for scrap cars Mattapoisett Massachusets.
There is no need to worry because we will do our best to surprise our customers from our work. as soon as possible is the best day to call us and get cash for your scrap car Mattapoisett MA. We offer cash in the moment that will be towed. Doesn't matter that in which condition your cars is or you are going to sell it, leave it to us, we will handle it with scrap cars For cash Mattapoisett MA experts.Money for junk cars Mattapoisett MA.
We Buy junk cars Mattapoisett Massachusets. The gas mileage decreases in older cars, and repair prices increase. To resolve all these problems Call us fast, We Buy scrap cars Mattapoisett Massachusets and we paid money. We provide fast service and pay cash. There is no need to wait several days; we will remove your scrap car within 5 to 48 hours in Mattapoisett Massachusets. Stop worrying about the cars taking up space in Mattapoisett Massachusets by contacting us asap money For junk cars Mattapoisett Massachusets
Say goodbye to your repair bills and get paid fast! scrap cars Removal Mattapoisett Massachusets is a company with a lot of years of experience in field of junk cars removing. Simply contact us and we'l schedule a time to come pick up your junk car in Mattapoisett MA. If you are in need to find best junk car removal service in Mattapoisett MA, then we are present to solve your problem. Free of charge and free removal, you will get your scrap cars towed, provided by one flatbed tow truck in Mattapoisett MA to a junk yard.
We proudly say that our service growing super fast in Mattapoisett Massachusets day by day and our customers are 110% happy. Free scrap cars Removal Mattapoisett MA ambition is to provide fast, hassle free scrap cars Removal service in Mattapoisett Massachusets as well as best customers service in every step of the way. Free scrap cars Removal Mattapoisett Massachusets offer free of cost which will be easy to save your money. We are doing our best to provide more convenience and better service to help you out. Our company made it too easy to remove your Free scrap cars as soon as we receive your phone call. It's our duty to take care all loading and removing your Free junk car Removal Mattapoisett MA. Cash for junk cars Mattapoisett MA.
We are ready to pick up your junk car and pay money for It even if you lost the title. Our service offers totally free removing service in Mattapoisett MA. Schedule your free junk cars removal in Mattapoisett MA asap! scrap car, old car, wrecked car to be recycled as environmentally-friendly in Mattapoisett Massachusets process and recycles vehicle fluids and hazardous material from your scrap cars. Have your scrap towed away from your property in Mattapoisett Massachusets to the junkyard. contact us to junk your cars asap. If you have an old cars, truck or van which requires a Free junk cars removal then contacts us today. Our service provide very super fast removing service.junk cars no title in Mattapoisett MA! Junk cars Removal without title Mattapoisett Massachusets


text: Random.org is used for holding drawings, lotteries and sweepstakes, to drive games and gambling sites, for scientific applications and for art and music. It offers true random numbers to anyone on the Internet. Random numbers are generated based on atmospheric noise. They have free tools e.g. flip coins, shuffle cards, and roll dice. It offers paid services to generate sequences of random numbers and act as a third-party arbiter for raffles, sweepstakes, and promotions. more


text:
The Basilica di Santa Maria del Fiore (in English, the Basilica of St. Mary of the Flower) is the mother church of the Archdiocese of Florence, in Italy. Constructed in the 14th century, it replaced a fifth-century church on the same spot which was crumbling with age.The Basilica, with its tall Baptistery of St. John adjacent to the main church, is one of the world's largest houses of worship. Particularly noteworthy is its Duomo (Dome), which was for centuries the largest dome in the wo … [Read more...]
How Did Florence's Medieval Builders Construct the World's Biggest Dome?
September 10, 2014 by 9 Comments
The Brindellone: Florence's "Burst of Cart" Heralds the Easter Season
April 14, 2012 by Leave a Comment
The eleventh century was a difficult time for Christians in Europe. Muslims had conquered the Levant—a far-reaching geographic region which encompasses modern-day Lebanon, Syria, Jordan, Israel, the Palestinian territories, and parts of Cyprus, Turkey and Iraq. The Holy Land, that part of the world where Jesus had walked and worked His miracles, was closed to Christians.Byzantine Emperor Alexius I Komnenos appealed to Pope Urban II, asking for western volunteers to help repel the invading S … [Read more...]


text:
Mary Anne's Grief (I)
Chapter Three: Grief – Mary Anne
The Laundry
The best beds in the entire institution were here. Too bad all that accompanied Mary Anne were eleven hours of crippling agony. Ripples, waves, torrents of pain rolling through her body.
Her throat was dry and aching, yet she couldn't hold back the screams that let rip with each contraction. Someone was holding her hand. She assumed it was Ellen, as she had been present when labour had started, but Mary Anne's head was so far in the clouds of agony that she barely reconized her friend.
"Come on, Mary, almost there, pet." Ellen was crying. Mary Anne had heard her crying in bed at night. Ellen probably couldn't even hear herself sobbing, poor thing. Her brain fog lifting slightly, Mary Anne took comfort in the fact that her screaming probably wasn't affecting her friend too badly, given her poor hearing. A pretty sick, desperate comfort to take, but given the current situation she had to clutch at every straw thrown her way.
"Gaaaaaaaaaaaaah!" Mary Anne roared as yet another agonizing contraction riveted her body. She felt Ellen's hard grow tighter. Or was it Mary Anne who was squeezing? She truly couldn't tell.
"Ellen," she whispered. "You should go. Sleep. You don't have to stay up. If you get caught, they'll –"
"None of that," Ellen snapped. Mary Anne was used to her friend being so quiet and reserved. Now she was in an almost authoritive mode. "I'm not going to be able to sleep if you're up here alone. Besides, everyoneelseis sleeping. The only way I'll get caught is if you wake them up with all that screaming."
Mary Anne couldn't bring herself to appreciate the humour. She let her head roll back and shut her eyes.
"Oh, my God, Mary Anne," came Ellen's now high-pitched, ecstatic voice. "Mary, I can see a head!"
"Yes, Ellen, babies have heads, aaaaaaaaaaaagh!" Mary Anne shouted, her words turning into an agonizing ringing. She breathed heavily. "Ellen," she whimpered, pulling her friend's arm so that she was leaning closer to her face. "Ellen, I can't do it."
"Yes, you can." Ellen stroked Mary Anne's dark, sweat-soaked hair. "You're the strongest person I know, Mary. And just think… It's a baby," she said, laughing with what cuold have been nerves or excitement.
Whatever it was, Mary Anne found herself smiling back through her pain. Ellen was right. This was her baby. The reason she was here in the first place. She couldn't give up.
"And anyway, pet, I don't think you have much choice," Ellen added.
"Oh, Ellen!" Mary Anne wailed, though there were still the slightest droplets of laughter in her tone.
Ellen smiled and shuffled back towards the end of the bed, still holding Mary Anne's hand despite the fact that both their hands were sweaty and slippery and the girls should technically have not been able to hold onto each other. Somehow Mary Anne and Ellen managed it.
Mary Anne screamed again.


text:
Go Have Breakfast
You slip out of bed, jog down the steps, and enter your kitchen. You open a light brown cabinet and pull a box of Yogurt Burst Cheerios. You place the box on the round table in the center of the kitchen. You grab a carton of milk from your refrigerator and a bowl from another cabinet.
As you prepare your cereal, you notice a picture on the back of your milk carton with the heading: MISSING.
You instantly notice that the picture is of your best friend, Diana.


text:
anyone know why the display suddenly goes into vertical lines, wide bars?
2 Replies
· · ·
May 6, 2011 at 9:07 UTC
I don't know anything about the smart uf55. I would double-check that Windows is using the right resolution and refresh rate for the unit.
If it is an LCD projector, which I think do exist, lines are often a sign of a bad panel, meaning chuck the think into the recycling pile and get a new one if reseating everything doesn't clear it up.
· · ·
May 9, 2011 at 1:41 UTC
We have one of those but have not seen that issues. Since it is a short through projector, my guess it it might be the bulb assembly or the unit unit its self is going out. Have you contacted Smart support as I have had pretty good luck dealing with them directly.


text:
- Cute otter face and body.
- Perfect gift for the nature lover.
- Durable and detailed.
- Description
- Reviews
- Shipping Information
No need to hide that boring tape dispenser anymore. Simply add a roll of tape to Otto the Otter and let him add a touch of whimsy to your desk or workspace.
Otto cradles your tape roll in his tummy and paws so reminiscent of how real otters eat and play.
Made from durable resin, you'll be amazed at how detailed Otto is. From his 'fur' to his expressive face, Otto is simply irresistible.
Otto is the cutest tape dispenser you'll ever see – just ask him! He 'otto' know!
Otto the Otter Tape Dispenser Features:
- Material: Poly Resin.
- Packaged in a color gift box.
- Size: 3.5"H x 6"L x 3.25"W
- Designed by Audra Langdon/USA.
For domestic (Contiguous US states) orders we now offer FREE Shipping on any order above $35.
While free shipping is great and cost effective, we realize that sometimes our customers only need fewer items. We therefore offer a low flat fee of $5 for Economy Shipping (5-10 Business Days) within the Contiguous US States) for all those orders that are not within the $35 threshold.
In most cases, we use USPS, FEDEX or UPS services to ship your order. Orders generally ship within 24 hours. Delivery time varies according to your choice of shipping method at checkout. Once your order ships, you will receive a shipping confirmation email with a tracking number so that you can follow the package wherever it is :).
Your satisfaction is important to us. We offer a 30 Day Guarantee Return Policy. If you are not happy with your purchase, just return it in new condition for a refund/replacement. Please review our Return Policy for more details. Terms and Conditions may apply.
Related Articles{{/articles.length}} {{#articles}}


text:
Hello. Sign In
Please enter a valid city, state or zip code
12 reviews | 2.9 out of 5
The panasonic wifi Lan Adaptor didn't work on the Panasonic BluRay player that I own. It calls for one, but, it will only work with a direct connection.
I will return it. The price was right. The delivery was great. It just didn't work on my model.
This wi-fi adaptor works great with your existing wireless network.
Even though my TC-P50GT25 TV is 40 feet away from my wireless router and I occasionally have issues connecting on my laptop from that location, I was able to connect easily to my wireless network using this adaptor. I am able to view movies from Netflix, Amazon Video on Demand and YouTube without any stuttering or delays over the last month that I have had this.
The only downside is that sometimes it takes a few minutes to reconnect with my wireless network after powering on the TV. Also reduced one star on the "Value" rating due to the fact that it was not bundled with the TV and had to shell out money separately for it.
Have a Panasonic Blu-ray player and this is the only wireless adapter that it will work with. Sadly, this item does not do the job. The DVD player recognizes it right away, but the adapter will not pick up any wireless signal. In spite of moving it to various spots it never locates a wireless signal. I had read poor reviews in other websites, but as I said, this was the only one which Panasonic Blu-Ray players will recognize.
Had no problem with this picking up my wi-fi signal (yes, you have to have wi-fi). I did have to contact AT&T to figure out how to set up a connection password for it.
The instant access to Netflix is fantastic. This works so well I'm getting another one for my other television.
This item worked with my netgear router and my Panasonic Blue Ray player and Panasonic 50 inch Plasma tv and Wireless speaker system. I was able to stream Netflix movies. I think it is just a matter of having the right networkconnection from router.
Horrible signal connection, it just simply doesn't work. It wouldn't be so bad that it's totally proprietary if it actually worked and made the player usable. I am returning this and the blu ray player.
This adapter is broken. It does not work with WPA2. And it does not work on 5ghz on 802.11n. I tried in on two different routers and it did not work on both.
Extremely satisfied! Worked first time and everytime flawlessly! Purchasing a second unit for my Panasonic 65" 3d Plasma!
Really easy to use and set up. Also much better than most wireless adapter for TVs.
does not work!!!