PotentialDeadlock.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.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF.ExpressionKind;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.SendLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF.LocationKind;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
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;

public class PotentialDeadlock implements TASSPredicateIF {

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

	public PotentialDeadlock(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 PotentialDeadlock(ModelIF model, int bufferBound,
			DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
			LogIF log) {
		ModelSequence modelSequence = new ModelSequence(model);

		this.model = 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;
	}

	private boolean synchronouslyEnabled(int senderPid, SendStatementIF send)
			throws ExecutionException, DynamicException {
		ValueIF sendDestinationValue = evaluator.evaluate(environment, send
				.destination());
		ValueIF assumption = environment.getAssumption();
		int sendDestinationPid = ((IntegerNumberIF) dynamicFactory
				.numericValue(assumption, sendDestinationValue)).intValue();
		ValueIF sendTagValue = evaluator.evaluate(environment, send.tag());
		int sendTag = ((IntegerNumberIF) dynamicFactory.numericValue(
				assumption, sendTagValue)).intValue();
		ProcessIF receiver = model.process(sendDestinationPid);
		LocationIF receiveLocation = environment.location(receiver);

		if (receiveLocation == null
				|| receiveLocation.kind() != LocationKind.RECEIVE)
			return false;
		for (StatementIF statement : receiveLocation.statements()) {
			ReceiveStatementIF receive = (ReceiveStatementIF) statement;
			ValueIF sourceValue = evaluator.evaluate(environment, receive
					.source());
			int sourcePid = ((IntegerNumberIF) dynamicFactory.numericValue(
					assumption, sourceValue)).intValue();

			if (sourcePid != senderPid) {
				continue;
			} else {
				ExpressionIF receiveTagExpression = receive.tag();

				if (receiveTagExpression.kind() == ExpressionKind.ANY) {
					return true;
				} else {
					ValueIF receiveTagValue = evaluator.evaluate(environment,
							receiveTagExpression);
					int receiveTag = ((IntegerNumberIF) dynamicFactory
							.numericValue(assumption, receiveTagValue))
							.intValue();

					if (receiveTag == sendTag)
						return true;
				}
			}
		}
		return false;
	}

	/**
	 * Returns true if the bad thing happens, i.e., if there is a potential
	 * deadlock.
	 */
	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)
			return false;
		for (int i = 0; i < numProcs; i++) {
			LocationIF location = environment.location(model.process(i));

			if (location == null)
				continue;

			try {
				switch (location.kind()) {
				case ALLOCATE:
				case ASSERTION:
				case ASSUME:
				case ASSIGNMENT:
				case RETURN:
					return false;
				case SEND: {
					SendStatementIF send = ((SendLocationIF) location)
							.statement();

					if (synchronouslyEnabled(i, send))
						return false;
					break;
				}
				default: {
					ValueIF predicate = null;
					ResultType truth;

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

						if (predicate == null)
							predicate = guard;
						else
							predicate = dynamicFactory.or(assumption,
									predicate, guard);
					}
					truth = dynamicFactory.valid(assumption, predicate);
					if (truth == ResultType.YES) {
						return false;
					} else if (truth == ResultType.MAYBE) {
						certainty = Certainty.MAYBE;
					}
				}
				}
			} catch (ExecutionException error) {
				log.report(error);
				environment.setAssumption(dynamicFactory.falseValue());
				return false;
			} catch (DynamicException error) {
				log.report(new ExecutionException(location, error,
						Certainty.NONE));
				environment.setAssumption(dynamicFactory.falseValue());
				return false;
			}
		}
		// made it to here means deadlock may be possible
		holdState = state;
		if (certainty == Certainty.PROVEABLE) {
			explanation = "Deadlock can occur";
		} else {
			explanation = "Cannot prove that deadlock is impossible";
		}
		explanation += " at " + state + ".";
		exception = new ExecutionStateException(environment.locations(),
				ErrorKind.DEADLOCK, certainty, explanation);
		log.report(exception);
		return true;
	}

	public String explanation() {
		if (holdState == null)
			return "No potential deadlock possible in this state.";
		else
			return explanation;
	}

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

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