AbsoluteDeadlock.java

package edu.udel.cis.vsl.tass.predicate.impl;

import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.predicate.IF.TASSPredicateIF;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.ErrorKind;
import edu.udel.cis.vsl.tass.state.States;
import edu.udel.cis.vsl.tass.state.IF.StateFactoryIF;
import edu.udel.cis.vsl.tass.state.IF.StateIF;
import edu.udel.cis.vsl.tass.state.IF.StatefulEnvironmentIF;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * An absolute deadlock occurs if all of the following hold:
 * 
 * <ol>
 * <li>not every process has terminated
 * <li>no process has an enabled statement (note that a send statement is
 * enabled iff the current number of buffered messages is less than the buffer
 * bound).
 * </ol>
 * 
 * It is to be contrasted with a "potentially deadlocked" state, i.e., one in
 * which there may be send transitions enabled, but the send transitions can
 * only execute if buffering is allowed, i.e., no matching receives are
 * currently posted. Every absolutely deadlocked state is potentially
 * deadlocked, but not necessarily vice-versa.
 * */
public class AbsoluteDeadlock implements TASSPredicateIF {

	private LogIF log;
	private StatefulEnvironmentIF environment;
	private ModelIF model;
	private EvaluatorIF evaluator;
	private int numProcs;
	private DynamicFactoryIF dynamicFactory;
	private ExecutionStateException exception;

	/**
	 * If the property holds (i.e., a deadlock has been detected at state), than
	 * the state is stored in this variable for future reference so that a nice
	 * "explanation" can be presented to the user.
	 */
	private StateIF holdState = null;

	// when buffer size = 0, allow synch? No.

	public AbsoluteDeadlock(ModelIF model, DynamicFactoryIF dynamicFactory,
			StatefulEnvironmentIF environment, EvaluatorIF evaluator,
			LogIF log) {
		this.model = model;
		this.dynamicFactory = dynamicFactory;
		this.numProcs = model.numProcs();
		this.environment = environment;
		this.evaluator = evaluator;
		this.log = log;
	}

	public AbsoluteDeadlock(ModelIF model, int bufferBound,
			DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
			LogIF log) {
		ModelSequence modelSequence;

		this.model = model;
		modelSequence = new ModelSequence(model);
		this.dynamicFactory = dynamicFactory;
		this.numProcs = model.numProcs();
		this.environment = States.newEnvironment(modelSequence, stateFactory,
				log);
		this.evaluator = Semantics.newEvaluator(dynamicFactory, bufferBound,
				log);
		this.log = log;
	}

	/** Is the given state an absolutely deadlocked state? */
	public boolean holdsAt(StateIF state) {
		boolean terminated = true;
		ValueIF assumption;
		Certainty certainty = Certainty.PROVEABLE;

		holdState = null;
		exception = null;
		environment.setState(state);
		assumption = environment.getAssumption();
		for (int i = 0; i < numProcs; i++) {
			if (environment.stackSize(model.process(i)) != 0) {
				terminated = false;
				break;
			}
		}
		if (terminated) // all processes terminated: no deadlock
			return false;
		for (int i = 0; i < numProcs; i++) { // is any process enabled?
			LocationIF location = environment.location(model.process(i));

			if (location == null)
				continue;
			switch (location.kind()) {
			case ASSERTION:
			case ASSUME:
			case ASSIGNMENT:
			case ALLOCATE:
			case RETURN:
				return false;
			default: {
				/* The predicate holds iff some statement enabled */
				ValueIF predicate = null;

				for (StatementIF statement : location.statements()) {
					try {
						ValueIF guard = evaluator.evaluate(environment,
								statement.guard());

						if (predicate == null) {
							predicate = guard;
						} else {
							predicate = dynamicFactory.or(assumption,
									predicate, guard);
						}
					} catch (ExecutionException error) {
						log.report(error);
						environment.setAssumption(dynamicFactory.falseValue());
						return false;
					} catch (DynamicException error) {
						log.report(new ExecutionException(statement, error,
								Certainty.NONE));
						environment.setAssumption(dynamicFactory.falseValue());
						return false;
					}
				}
				try {
					if (predicate != null) {
						ResultType truth = dynamicFactory.valid(assumption,
								predicate);

						if (truth == ResultType.YES) {
							return false;
						} else if (truth == ResultType.MAYBE) {
							certainty = Certainty.MAYBE;
						} else {
							// for some input, no statement is enabled for this
							// proc
						}
					}
				} catch (DynamicException error) {
					log.report(new ExecutionStateException(environment
							.locations(), error, Certainty.NONE));
					environment.setAssumption(dynamicFactory.falseValue());
					return false;
				}
			}
			}
		}
		// if made it here: deadlock might be possible
		holdState = state;
		String message;

		if (certainty == Certainty.MAYBE)
			message = "Cannot prove that deadlock is impossible:";
		else
			message = "A deadlock is possible:";
		message += explanation();
		exception = new ExecutionStateException(state.locations(),
				ErrorKind.DEADLOCK, certainty, message);
		log.report(exception);
		return true;
	}

	/**
	 * Returns a user-friendly explanation of why this is a deadlocked state.
	 * Reads the holdState variable. Should only be called immediately after
	 * holdsAt has returned true.
	 */
	public String explanation() {
		StateIF state = holdState;
		ValueIF assumption;
		String explanation;

		if (holdState == null)
			return "No deadlock possible at this state.";
		explanation = "Absolute deadlock possible at " + state + ".\n";
		environment.setState(state);
		assumption = environment.getAssumption();
		for (int i = 0; i < numProcs; i++) {
			LocationIF location = environment.location(model.process(i));
			ValueIF predicate = null;

			explanation += "Process " + i + ": ";
			if (location == null) {
				explanation += "terminated\n";
			} else {
				explanation += "at location " + location.id() + ".  ";
				try {
					for (StatementIF statement : location.statements()) {
						ValueIF guard = evaluator.evaluate(environment,
								statement.guard());

						if (predicate == null) {
							predicate = guard;
						} else {
							predicate = dynamicFactory.or(assumption,
									predicate, guard);
						}
					}
				} catch (ExecutionException error) {
					explanation += "\n" + error;
				} catch (DynamicException error) {
					explanation += "\n" + error;
				}
				if (predicate == null) {
					explanation += "No outgoing transitions.\n";
				} else {
					explanation += "Cannot prove enabling statement valid:\n"
							+ predicate + "\n";
				}
			}
		}
		return explanation;
	}

	public String toString() {
		return "AbsoluteDeadlock";
	}

	@Override
	public ExecutionStateException getException() {
		return exception;
	}
}