LibmpiExecutor.java

package edu.udel.cis.vsl.tass.library.libmpi;

// a work in progress...

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.type.ArrayValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.MessageIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ReferenceValueIF;
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.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.statement.InvocationStatementIF;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.semantics.IF.EnvironmentIF;
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.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
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.semantics.impl.Evaluator;
import edu.udel.cis.vsl.tass.util.Sourceable;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

public class LibmpiExecutor implements LibraryExecutorIF {

	public final static int MPI_INT = 1;
	public final static int MPI_FLOAT = 2;
	public final static int MPI_DOUBLE = 3;
	public final static int MPI_CHAR = 4;
	public final static int MPI_BYTE = 5;

	public final static int MPI_COMM_WORLD = 1;

	private ExecutorIF executor;

	private Evaluator evaluator;

	private DynamicFactoryIF dynamicFactory;

	private LogIF log;

	ValueIF falseValue, oneInt, commWorld;

	public LibmpiExecutor(ExecutorIF executor, EvaluatorIF evaluator) {
		this.executor = executor;
		this.evaluator = (Evaluator) evaluator;
		this.dynamicFactory = evaluator.dynamicFactory();
		this.log = evaluator.log();
		this.falseValue = dynamicFactory.falseValue();
		this.oneInt = dynamicFactory.one();
		this.commWorld = dynamicFactory.symbolicValue(MPI_COMM_WORLD);
	}

	@Override
	public boolean containsFunction(String name) {
		if ("MPI_Recv".equals(name) || "MPI_Send".equals(name))
			return true;
		return false;
	}

	@Override
	public void execute(EnvironmentIF environment,
			InvocationStatementIF statement) throws ExecutionException {
		try {
			LocationIF targetLocation = statement.targetLocation();
			ProcessIF process = statement.process();
			String name = statement.callee().name();

			if (name.equals("MPI_Recv")) {
				// executeRecv(environment, statement);
			} else if (name.equals("MPI_Send")) {
				executeSend(environment, statement);
			} else {
				throw new ExecutionException(statement, ErrorKind.LIBRARY,
						Certainty.MAYBE, "Unknown function: " + name);
			}
			environment.setLocation(process, targetLocation);
		} catch (DynamicException e) {
			throw new ExecutionException(statement, e, Certainty.NONE);
		}
	}

	// create message and insert in queue.
	// the message data will always be in the form of an array of elements of
	// some type.

	// int MPI_Send(void* _buf, int _count, MPI_Datatype _datatype, int _dest,
	// int _tag,
	// MPI_Comm _comm)

	private void checkComm(ValueIF commValue, Sourceable sourceable)
			throws ExecutionException {
		if (!commWorld.equals(commValue)) {
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.MAYBE,
					"Currently TASS only supports communicator MPI_COMM_WORLD:"
							+ "\n    MPI_COMM_WORLD : " + commWorld
							+ "\n      communicator : " + commValue);
		}
	}

	private void executeSend(EnvironmentIF environment,
			InvocationStatementIF statement) throws DynamicException,
			ExecutionException {
		ValueIF assumption = environment.getAssumption();
		ModelIF model = statement.model();
		ProcessIF sourceProcess = statement.process();
		ExpressionIF[] arguments = statement.arguments();
		ReferenceValueIF buffer;
		ValueIF countValue, datatypeValue, destinationValue, tagValue, commValue;
		ArrayValueIF dataValue;
		ProcessIF destinationProcess;
		MessageIF message;
		IntegerNumberIF pidNumber;

		buffer = (ReferenceValueIF) evaluator.evaluate(environment,
				arguments[0]);
		countValue = evaluator.evaluate(environment, arguments[1]);
		datatypeValue = evaluator.evaluate(environment, arguments[2]);
		destinationValue = evaluator.evaluate(environment, arguments[3]);
		tagValue = evaluator.evaluate(environment, arguments[4]);
		commValue = evaluator.evaluate(environment, arguments[5]);
		checkComm(commValue, arguments[5]);
		pidNumber = (IntegerNumberIF) dynamicFactory.numericValue(assumption,
				destinationValue);
		if (pidNumber != null) {
			int pid = pidNumber.intValue();

			if (pid < 0 || pid >= model.numProcs()) {
				log.report(new ExecutionException(statement,
						ErrorKind.INVALID_PID, Certainty.PROVEABLE,
						"Invalid destination value in send (" + pid
								+ ") for model " + model.name() + " with "
								+ model.numProcs() + " processes"));
				environment.setAssumption(falseValue);
				return;
			}
			destinationProcess = model.process(pid);
		} else {
			log.report(new ExecutionException(statement, ErrorKind.INTERNAL,
					Certainty.MAYBE,
					"Destination process cannot be resolved to concrete value: "
							+ destinationValue));
			environment.setAssumption(falseValue);
			return;
		}

		// check that the buffer actually contains the kinds of elements
		// indicated
		// by datatypeValue. Example: datatypeValue is MPI_DOUBLE. Then the
		// buffer must be a pointer to double. If count is 0, fine.
		// If count is one, buffer can be pointer of any kind as long as not
		// pointing off end of variable or array. If count is 2 or higher,
		// it must be to an element of an array and must prove the length
		// of the array is as required to accommodate count elements. Failure
		// to establish these things yields in error log. Recover if possible.

		// create an array of length count, datatype same as elements

		dataValue = extractData(environment, assumption, buffer, countValue,
				datatypeValue, statement);
		message = dynamicFactory.message(sourceProcess, destinationProcess,
				tagValue, dataValue);
		environment.enqueue(message);
	}

	private int datatypeInt(ValueIF assumption, ValueIF datatypeValue,
			Sourceable sourceable) throws DynamicException, ExecutionException {
		IntegerNumberIF datatypeNumber = (IntegerNumberIF) dynamicFactory
				.numericValue(assumption, datatypeValue);

		if (datatypeNumber == null)
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.NONE, "Unable to decode datatype: "
							+ datatypeValue);
		return datatypeNumber.intValue();
	}

	private ValueIF modifiedCount(EnvironmentIF environment,
			ValueIF assumption, ValueIF datatypeValue,
			ValueTypeIF elementValueType, ValueIF countValue,
			Sourceable sourceable) throws DynamicException, ExecutionException {
		int datatypeInt = datatypeInt(assumption, datatypeValue, sourceable);
		ValueTypeIF datatypeValueType;

		switch (datatypeInt) {
		case MPI_INT:
			datatypeValueType = dynamicFactory.integerType();
			break;
		case MPI_DOUBLE:
		case MPI_FLOAT:
			datatypeValueType = dynamicFactory.realType();
			break;
		case MPI_CHAR:
			datatypeValueType = dynamicFactory.characterType();
			break;
		case MPI_BYTE: {
			/* use whatever the buffer element type is */
			ValueIF sizeofElement = dynamicFactory.sizeof(elementValueType);
			ValueIF claim = dynamicFactory.divides(assumption, sizeofElement,
					countValue);
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				ExecutionException error;
				Certainty certainty;
				String message;

				if (truth == ResultType.MAYBE) {
					certainty = Certainty.MAYBE;
					message = "Unable to prove that count is multiple of size of a buffer element:";
				} else {
					certainty = Certainty.PROVEABLE;
					message = "It is possible for the count to not be a multiple of"
							+ "\nthe size of a buffer element:";
				}
				message += "\n        count    : " + countValue
						+ "\n element type    : " + elementValueType
						+ "\n size of element : " + sizeofElement
						+ "\n  path condition : " + assumption;
				error = new ExecutionException(sourceable,
						ErrorKind.COMMUNICATION, certainty, message);
				log.report(error);
				try {
					environment.addAssumption(claim);
				} catch (ExecutionProblem e) {
					throw new ExecutionException(sourceable, e);
				}
			}
			countValue = dynamicFactory.intDivide(assumption, countValue,
					sizeofElement);
			datatypeValueType = elementValueType;
		}
		default:
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.MAYBE, "Unrecognized datatype value: "
							+ datatypeInt);
		}
		if (!elementValueType.equals(datatypeValueType)) {
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.MAYBE,
					"Type of elements in buffer may not correspond to"
							+ "\nspecified MPI datatype:"
							+ "\n element type    : " + elementValueType
							+ "\n MPI datatype    : " + datatypeValueType);
		}
		return countValue;
	}

	private ArrayValueIF extractData(EnvironmentIF environment,
			ValueIF assumption, ReferenceValueIF buffer, ValueIF countValue,
			ValueIF datatypeValue, Sourceable sourceable)
			throws ExecutionException, DynamicException {
		ArrayValueIF result = null;
		ValueTypeIF elementValueType = buffer.valueType().baseType();

		countValue = modifiedCount(environment, assumption, datatypeValue,
				elementValueType, countValue, sourceable);
		if (buffer instanceof ArrayElementReferenceValueIF) {
			ValueIF indexValue = ((ArrayElementReferenceValueIF) buffer)
					.index();

			if (dynamicFactory.isValid(assumption, dynamicFactory.equals(
					assumption, dynamicFactory.zero(), indexValue))) {
				ReferenceValueIF arrayReference = buffer.parent();
				ArrayValueIF arrayValue = (ArrayValueIF) evaluator.dereference(
						environment, arrayReference, sourceable);
				ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) arrayReference
						.valueType().baseType();
				ValueIF extent = arrayValueType.extent();

				if (dynamicFactory.isValid(assumption, dynamicFactory.equals(
						assumption, countValue, extent))) {
					result = arrayValue;
				}
			}
		}
		if (result == null) {
			// need to get slice of array or read each value
			IntegerNumberIF countNumber = (IntegerNumberIF) dynamicFactory
					.numericValue(assumption, countValue);
			int count;
			ValueIF[] messageElements;
			ArrayValueTypeIF messageType;

			if (countNumber == null) {
				throw new ExecutionException(sourceable,
						ErrorKind.COMMUNICATION, Certainty.NONE,
						"Unable to get concrete value from count: "
								+ countValue);
			}
			count = countNumber.intValue();
			messageElements = new ValueIF[count];
			for (int i = 0; i < count; i++) {
				messageElements[i] = evaluator.dereference(environment, buffer,
						sourceable);
				buffer = evaluator.evaluatePointerAdd(environment, buffer,
						oneInt, sourceable);
			}
			messageType = dynamicFactory.arrayValueType(elementValueType,
					countValue);
			result = dynamicFactory.arrayValue("message", messageType,
					messageElements);
		}
		return result;
	}

	@SuppressWarnings("unused")
	private void copyDataToBuffer(EnvironmentIF environment,
			ValueIF assumption, ArrayValueIF data, ReferenceValueIF buffer,
			ValueIF countValue, ValueIF datatypeValue, Sourceable sourceable)
			throws ExecutionException, DynamicException {
		ArrayValueTypeIF dataValueType = data.valueType();

		assert dataValueType.dimension() == 1;

		ValueTypeIF dataElementType = dataValueType.baseType();
		ValueTypeIF bufferElementType = buffer.valueType().baseType();

		countValue = modifiedCount(environment, assumption, datatypeValue,
				bufferElementType, countValue, sourceable);

		if (!dataElementType.equals(bufferElementType)) {
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.MAYBE,
					"Element type of incoming message does not match element type of buffer:"
							+ "\n     message element type : "
							+ dataElementType
							+ "\n      buffer element type : "
							+ bufferElementType);
		}
		// if buffer is pointer to first element of array of extent count, ok

		if (buffer instanceof ArrayElementReferenceValueIF) {
			ValueIF indexValue = ((ArrayElementReferenceValueIF) buffer)
					.index();

			if (dynamicFactory.isValid(assumption, dynamicFactory.equals(
					assumption, dynamicFactory.zero(), indexValue))) {
				ReferenceValueIF arrayReference = buffer.parent();
				ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) arrayReference
						.valueType().baseType();
				ValueIF extent = arrayValueType.extent();

				if (dynamicFactory.isValid(assumption, dynamicFactory.equals(
						assumption, countValue, extent))) {
					executor.assignValue(environment, arrayReference, data,
							sourceable);
					return;
				}
			}
		}

		IntegerNumberIF countNumber = (IntegerNumberIF) dynamicFactory
				.numericValue(assumption, countValue);
		int count;

		if (countNumber == null) {
			throw new ExecutionException(sourceable, ErrorKind.COMMUNICATION,
					Certainty.NONE, "Unable to get concrete value from count: "
							+ countValue);
		}
		count = countNumber.intValue();
		for (int i = 0; i < count; i++) {
			ValueIF index = dynamicFactory.symbolicValue(i);
			ValueIF datum = dynamicFactory.arrayRead(assumption, data, index);

			executor.assignValue(environment, buffer, datum, sourceable);
			buffer = evaluator.evaluatePointerAdd(environment, buffer, oneInt,
					sourceable);
		}
	}

	// oops: no way to execute wildcard receive: nondeterminism.

	// private void executeRecv(EnvironmentIF environment,
	// InvocationStatementIF statement) throws ExecutionException {
	//
	// ProcessIF destinationProcess = statement.process();
	// ValueIF assumption = environment.getAssumption();
	// ModelIF model = statement.model();
	// ExpressionIF[] arguments = statement.arguments();
	// ReferenceValueIF buffer;
	// ValueIF countValue, datatypeValue, sourceValue, tagValue, commValue;
	// ReferenceValueIF statusReference;
	// ArrayValueIF dataValue;
	// ProcessIF sourceProcess;
	// MessageIF message;
	// IntegerNumberIF pidNumber;
	//
	// buffer = (ReferenceValueIF) evaluator.evaluate(environment,
	// arguments[0]);
	// countValue = evaluator.evaluate(environment, arguments[1]);
	// datatypeValue = evaluator.evaluate(environment, arguments[2]);
	// sourceValue = evaluator.evaluate(environment, arguments[3]);
	// tagValue = evaluator.evaluate(environment, arguments[4]);
	// commValue = evaluator.evaluate(environment, arguments[5]);
	// checkComm(commValue, arguments[5]);
	// statusReference = (ReferenceValueIF) evaluator.evaluate(environment,
	// arguments[6]);
	// // pidNumber = (IntegerNumberIF) dynamicFactory.numericValue(assumption,
	// // sourceValue);
	//
	// // if (sourceExpression.kind() == ExpressionKind.ANY) {
	// // log.report(new ExecutionException(sourceExpression,
	// // ErrorKind.COMMUNICATION, Certainty.NONE,
	// // "Source expression in receive should not use \"any\""));
	// // environment.setAssumption(falseValue);
	// // return;
	// // }
	// // sourceValue = evaluator.evaluate(environment, sourceExpression);
	// // pidNumber = (IntegerNumberIF) dynamicFactory.numericValue(
	// // assumption, sourceValue);
	// // if (pidNumber != null) {
	// // int pid = pidNumber.intValue();
	// //
	// // if (pid < 0 || pid >= model.numProcs()) {
	// // log.report(new ExecutionException(statement,
	// // ErrorKind.INVALID_PID, Certainty.PROVEABLE,
	// // "Illegal source value in receive (" + pid
	// // + ") for model " + model.name() + " with "
	// // + model.numProcs() + " processes"));
	// // environment.setAssumption(falseValue);
	// // return;
	// // }
	// // sourceProcess = model.process(pid);
	// // } else {
	// // log.report(new ExecutionException(statement,
	// // ErrorKind.INTERNAL, Certainty.MAYBE,
	// // "Source process cannot be resolved to concrete value: "
	// // + sourceValue));
	// // environment.setAssumption(falseValue);
	// // return;
	// // }
	// // if (tagExpression.kind() == ExpressionKind.ANY) {
	// // tagValue = null;
	// // tagLHS = (LHSExpressionIF) ((UnaryExpressionIF) tagExpression)
	// // .expression();
	// // } else {
	// // tagValue = evaluator.evaluate(environment, tagExpression);
	// // }
	// // message = environment.dequeue(sourceProcess, destinationProcess,
	// // tagValue);
	// // if (message == null)
	// // throw new RuntimeException(
	// // "TASS internal error: no message to receive: "
	// // + statement);
	// // if (tagLHS != null)
	// // assignValue(environment, tagLHS, message.tag());
	// // data = message.data();
	//
	// }

	@Override
	public String name() {
		return "libmpi";
	}

	@Override
	public void initialize(EnvironmentIF environment) throws ExecutionException {
		// TODO Auto-generated method stub
	}

	@Override
	public void wrapUp(EnvironmentIF environment) throws ExecutionException {
		// TODO Auto-generated method stub
		// check there are no outstanding requests, no unreceived messages, ...
	}
}