Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha128a/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha128a/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========

(1) A bug in metaParseStrategy(), found and fixed by Rubén.
Demonstrated by:

red in META-LEVEL : metaParseStrategy(['NAT], none, 'top '`( 'all '`)) .

(2) A bug where a cached simple parser was being used
with complex parser auxiliary information leading to crash.
Found by Rubén and demonstrated by:

select META-LEVEL .

red metaParse(upModule('NAT, false), none, '0, 'Nat) .
red metaParseStrategy(upModule('NAT, false), none, 'idle) .
red metaParse(upModule('NAT, false), none, '0, 'Nat) .

(3) A bug where signals such as ^C could be ignored if they arrived
after a global flag had been checked but before a blocking call to
poll(). This is resolved by using ppoll() on Linux and by a less
efficient implementation using the POSIX compliant pselect() on
non-Linux systems. It turns out that not losing signals due to this
race condition is critical for handling child processes in a
nonblocking way for the new process API (see below).

(4) A bug where sockets were broken if used in a full duplex manner;
that is having a pending read and a pending write on the same socket.

(5) A bug where Maude would fail to handle SIGPIPE when writing to a
socket whose other end was closed.

(6) The -help message has been corrected to include the -show-pid
command line flag rather than a nonexistent -get-pid flag. Spotted
by Rubén.

(7) A bug in the CU/U/Ul/Ur unification code where a f(...) =? X
subproblem would be solved using X rather than the representative
variable for X; in particular this could forget any binding to another
variable that X might have and generate non-unifiers. Provoked by:

fmod FOO is
  sort Small Foo .
  subsort Small < Foo .
  op 1 : -> Foo .
  op f : Foo Foo -> Foo [id: 1] .
  op g : Foo -> Foo .
vars X Y Z : Foo .
var S : Small .
endfm

unify Z =? f(X, Y) /\ g(Z) =? g(S) .

Here solution 3

Z --> f(#1:Foo, #2:Foo)
X --> #1:Foo
Y --> #2:Foo
S --> #3:Small

is not a unifier and arises because an earlier binding of Z |-> S
induced by g(Z) =? g(S) which makes S the representative variable
for Z has been overwritten.

(8) A bug where a collapse-up situation was not being detecting
if there was an operator declaration involving kinds; for example:

fmod FOO is
  sort Foo .
  op f : Foo [Foo] -> Foo [id: e] .
  op e : -> Foo .
endfm

parse f(e, X:[Foo]) .
red f(e, X:[Foo]) .

Here f(e, X:[Foo]) has a smaller sort than its collapse,
X:[Foo]. This is illegal since it breaks the computation
of the the miminal sort of a congruence class by computing
the sort of a maximally collapsed representative. This
case now generates a warning:

Warning: sort declarations for operator f with left identity
e can cause collapse from sort Foo to [Foo] (collapsing to a
larger or incomparable sort is illegal).

(9) A bug in the sort analysis phase that could cause
lost ACU unifiers. For example:

fmod FOO is
  sorts Zero NzNat Nat .
  subsorts Zero NzNat < Nat .
  op _+_ : Nat NzNat -> NzNat [assoc comm id: 0] .
  op _+_ : Nat Nat -> Nat [ditto] .
  op 0 : -> Zero .
  op g : Zero -> Nat .
endfm

unify N:Nat =? g(M:Nat + Z:Zero) .

Here no unifier was found, despite there being two order-sorted
mgus:

N:Nat --> g(#1:Zero)
M:Nat --> #1:Zero
Z:Zero --> 0

and

N:Nat --> g(#1:Zero)
M:Nat --> 0
Z:Zero --> #1:Zero

This situation arises because both of these solutions are
subsumed by the unsorted mgu:

N:Nat --> g(#1 + #2)
M:Nat --> #1
Z:Zero -->#2

as so are suppressed, but then the unsorted mgu cannot be
given a sorting so is killed in the order-sorting phase

I was aware that this could happen and indeed the ACU algorithm
has code to avoid lost unifiers in this situation. However the
ACU unification code depends on flags that were being incorrectly
set by the sort analysis code. It requires a carefully constructed
signature with at least two bottom sorts to exercise this bug.

(10) A bug in unifier filter code that caused silent memory
corruption. Caused by not accounting for abstraction variables for
earlier patterns (unifier bindings) when compiling latter patterns
during the subsumption check. Visible when compiled with DEBUG option
and illustrated by:

fmod A-UNIF is
  sorts List Elt .
  subsort Elt < List .
  op f : List List -> List [assoc] .
  op j : List List -> List [assoc comm id: 1] .
  op 1 : -> List .
  vars A B C D G H I 
       S U V W X Y Z : List .
  var E  : Elt .
endfm

variant unify j(A, f(B, E, C), f(D, E, j(G, H), I)) =?
  j(U, f(V, W), f(X, j(Y, Z), S)) .

(11) A symmetric bug in the variant folder code that became visible
with the same example when (10) was fixed.


New features
=============

(1) There is an experimental implementation of Unix
processes as Maude external objects. The API is contained
in process.maude

fmod STRING-LIST is
  protecting LIST{String} *
    (sort NeList{String} to NeStringList, sort List{String} to StringList) .
endfm

mod PROCESS is
  including SOCKET .
  protecting STRING-LIST .

  sorts ProcessOption ProcessOptionSet .
  subsort ProcessOption < ProcessOptionSet .
  op none : -> ProcessOptionSet [ctor] .

  sort ExitStatus .
  op normalExit : Nat -> ExitStatus [ctor] .
  op terminatedBySignal : String -> ExitStatus [ctor] .

  op process : Nat -> Oid [ctor] .

  op createProcess : Oid Oid String StringList ProcessOptionSet -> Msg [ctor msg format (b o)] .
  op createdProcess : Oid Oid Oid Oid Oid -> Msg [ctor msg format (m o)] .

  op signalProcess : Oid Oid String -> Msg [ctor msg format (b o)] .
  op signaledProcess : Oid Oid -> Msg [ctor msg format (m o)] .

  op waitForExit : Oid Oid -> Msg [ctor msg format (b o)] .
  op exited : Oid Oid ExitStatus -> Msg [ctor msg format (m o)] .

  op processError : Oid Oid String -> Msg [ctor msg format (r o)] .

  op processManager : -> Oid [special (...)] .
endm

New processes are created with the createProcess() message.
The arguments are:
  Oid		processManager (special builtin object)
  Oid		requesting object
  String	command the new process should execute
  StringList	arguments to the command
  ProcessOptionSet	reserved for future use; pass none

On success the reply is createdProcess(), with arguments:
  Oid	requesting object
  Oid	processManager (special builtin object)
  Oid	new process object using process() constructor
  Oid	new socket object for stdin/stdout
  Oid	new socket object for stderr

One can communicate with the new process using its stdin/stdout
socket and the normal socket interface defined in socket.maude
Errors can be read on the stderr socket. It's probably good
practice to always have receives pending on both sockets so
the process isn't stalled due to socket buffers filling.
The stderr socket ignores send() messages.

Maude will stop rewriting and return to the command line as
soon as there are no rewrites possible and no external events
pending that could change the rewrite state, even if the
newly created process is still running.

It's good practice to wait for a process to exit, if only to
avoid filling the process table with zombies. This is done
by sending the process a waitForExit() message. If this is done,
because there is a pending external event, Maude will not return
to the command line, until the process actually exits. When it
does, the reply message is exited(), with the last argument
being either normalExit() with an 8-bit exit code for a normal
exit or a terminatedBySignal() with the name of the signal
in the case of termination by signal. waitForExit() is
nonblocking so it can be sent anytime after the createdProcess()
message is received. A second waitForExit() message to the
same process will not be accepted.

When a process has been waited for, its stdin/stdout and stderr are
closed. It is the users responsibility to close the sockets
to avoid leaking file descriptors. One way to do this
is to keep receive()ing any final characters from the process
until an end-of-file or error condition arises and Maude returns
a closedSocket() message. Alternatively they can be sent
closeSocket() messages.

Different executables have different conventions for telling
them to quit. You can send a process the empty string to cause
an EOF condition on its stdin (see below). You can also send a
signal to a process using the signalProcess() message. The third
argument is a string with the name of the Unix signal.
Not every signal is supported by every platform and not every
signal makes sense to send to a child process. The follow POSIX
signals are supported on all Unix platforms; everything else
should be considered platform dependent.
  SIGHUP
  SIGINT
  SIGQUIT
  SIGKILL
  SIGALRM
  SIGTERM
  SIGSTOP
  SIGCONT
The reply is signaledProcess().

The message processError() is used as the reply for errors
coming from the operating system. In particular a processError()
reply is generated if the child process cannot execute the
specified executable.

Here's a trival example that invokes the dc (desk calculator)
program to do some calculations and then kills it with a
SIGTERM signal:

load process

mod TEST is
  inc PROCESS .
  op me : -> Oid .
  op User : -> Cid .
  op state:_ : Nat -> Attribute .
  op process:_ : Oid -> Attribute .
var X P ERR IO : Oid .
var Result : String .

  rl < X : User | state: 1 > createdProcess(me, processManager, P, IO, ERR) =>
     < X : User | state: 2, process: P > send(IO, me, "10 16 + p\n") waitForExit(P, me) .
  rl < X : User | state: 2, process: P > sent(me, IO) =>
     < X : User | state: 3, process: P > receive(IO, me) .
  rl < X : User | state: 3, process: P > received(me, IO, Result) =>
     < X : User | state: 4, process: P > send(IO, me, "4 * p\n") .
  rl < X : User | state: 4, process: P > sent(me, IO) =>
     < X : User | state: 5, process: P > receive(IO, me) .
  rl < X : User | state: 5, process: P > received(me, IO, Result) =>
     < X : User | state: 6, process: P > signalProcess(P, me, "SIGTERM") .
endm

erew <>
< me : User | state: 1 > 
createProcess(processManager, me, "dc", nil, none) .

When the current erewrite context is destroyed (say by
running a new rewrite command) Maude will kill any processes
and close any sockets that correspond to Maude external
objects in that context.

(2) There is a new command line flag
  -no-execute
that disables the createProcess() message.

Note that the ability to execute arbitrary code from Maude
greatly expands the possibilities for writing Maude malware
(that possibility already existed to a very slight extent
with internet sockets, and to a greater extent with the
ability to read and write files in the user's filesystem).
Be wary of running untrusted code without passing this
flag. Note that it is not sufficient merely to remove
process.maude since malware could have its own hooks into
the Maude process manager code.

(3) There is experimental support for unification modulo
associativity-identity. Currently only the two-sided identity
case is implemented. Associativity-identity, like associativity
is an infinitary theory and the implemented algorithm is
incomplete and will report incompleteness when it is
encountered. Currently the algorithm generates a lot of
redundant unifiers, though for the first cut I'm more concerned
about missing unifiers in cases where the algorithm claims to
be complete. There are a number of subtle issues: in particular
there are most general order-sorted unifiers that are not
most general unsorted unifiers which means just finding a
complete set of most general unsorted unifiers and then
computing sorts for the variables is insufficient.
For example:

fmod AU-SORTED1 is
  sorts Lo Hi .
  subsort Lo < Hi .
  op 1 : -> Hi .
  op f : Hi Hi -> Hi [assoc id: 1] .
endfm

unify X:Lo =? f(Y:Hi, Z:Hi) .

Here the non-collapse solution cannot be sorted so the collapse
solutions become mgus after order sorting. Also:

fmod AU-SORTED2 is
  sorts Lo Hi .
  subsort Lo < Hi .
  op 1 : -> Hi .
  op f : Hi Hi -> Hi [assoc id: 1] .
  op f : Lo Lo -> Lo [assoc id: 1] .
endfm

unify X:Lo =? f(Y:Hi, Z:Hi) .

Here the single unsorted mgu has a sorting, but this sorting
no longer subsumes the collapse solutions so they also become
mgus after order sorting.

The implementation handles subtle cases where the identity
contains the associative-identity operator itself:

fmod FOO is
  sort Foo .
  ops a b : -> Foo .
  op h : Foo -> Foo .
  op f : Foo Foo -> Foo [assoc id: h(f(a, b))] .

  vars X Y : Foo .
endfm

unify X =? f(Y, a, b) /\ Y =? h(X) .

As with unification in general, if you want to know how
many unifiers are in the minimal complete set of unifiers
for a problem (which is unique) you can use variant unify with
an empty set of variant equations. This works because variant
narrowing filters unifiers to remove redundant ones. For example:

fmod AU-TEST is
  sort Foo .
  op 1 : -> Foo .
  op __ : Foo Foo -> Foo [assoc id: 1] .
  ops a b c : -> Foo .
vars A B C X Y Z : Foo .
endfm

unify A B =? X Y .
*** 12 unifiers found - lots of redundant collapses

variant unify A B =? X Y .
*** only 2 are most general

This is an example where associativity-identity has fewer
most general unifiers than associativity which has 3. This
is because the "obvious" unifier is subsumed by both of
the two less obvious unifiers when identity is available.


Other changes
==============

(1) Strategy definitions now support the nonexec attribute.

(2) The handling of socket exception conditions has been cleaned up.

The new semantics is that an attempt to send() on a broken
connection will receive a socketError() reply, but the socket
will not be closed. This is so that any remaining incoming characters
in the socket can be retrieved.

An attempt to receive() on a broken connection will get any
remaining characters in a received() message. Once there are no
more characters, an attempt to receive() will be answered by
a closedSocket() message, and the external socket object will
disappear.

The API does not completely shield the user from the race condition
between attempts to read and write to a socket and the other
end of the socket being closed. In particular the String in a
socketError() or closedSocket() message depends on operating
system and the exact sequence of events. For example if you
have a receive() pending on a socket and it is disconnected with
no characters left in the socket it will normally treated as a
regular "end-of-file" type close and the message will look like:
  closedSocket(me, socket(3), "")
However if the other end of the socket has already been closed
before the receive() is attempted and there are no characters
to retrieve, most operating systems treat this as an ECONNRESET
error and the message will look like:
  closedSocket(me, socket(3), "Connection reset by peer")
In general the String in socketError() or closedSocket() messages
is for user information only and should not be relied on
programmatically.

(3) It is now possible to shutdown (with the Unix shutdown() system
call) the write half of a socket by send()ing the empty string.
This has the effect of creating an end-of-file condition for the
reader at the other end of the socket once any in-channel characters
have been read, and transforms the socket into a read-only socket
with further attempts to send() being ignored.
Previously attempts to send() the empty string were ignored.

(4) The AC(U) and A(U) unification code checks before making
bindings like:
  X:Foo |-> #42:[Foo]
during the construction of a local solution, where X is an original
variable and #42 a fresh variable created for a Diophantine basis
element (AC(U)) or word problem variable (A(U)) and reuses X in the
problem instead of creating #42:[Foo]. This has two potential
advantages: the number of variables in the problem is reduced, and
reusing X means that more accurate sort information, Foo rather than
[Foo], is avaiable to other unification subproblems which might cut
off fruitless searches. This also means that fresh variable numbering
is permuted.

(5) Sort bounds computed by the new version of PIG-PUG introduced
in alpha128 are now propagated between PIG-PUG runs for different
unification subproblems under the same associative symbol allowing
more finitary instances to be detected and solved completely. Consider

fmod TEST is
  sorts Elt Pair Triple List .
  subsort  Elt < Pair < Triple < List .
  op __ : Elt Elt -> Pair [assoc] .
  op __ : Elt Pair -> Triple [assoc] .
  op __ : Pair Elt -> Triple [assoc] .
  op __ : List List -> List [assoc] .

  var E F G : Elt .
  var P Q R : Pair .
  var T U V : Triple .
  var L M N : List .
endfm

unify L E =? E L .

This is a classic example of an infinitary unification instance.
But now if it is conjuncted with an instance that forces a bound
on L, the combined problem has a complete set of 8 most general
order-sorted unifiers.

unify L E =? E L /\ P L =? Q T .

The new version will find them all without declaring incompleteness.
Previously Maude would not propagate the bounds on L computed for
each of the 3 solutions of P L =? Q T and thus would only find 5
solutions of the whole and declare incompleteness.

Steven