Hello Narayan, Ed, Paul: Thanks for responding to my question. I believe
a common concern is Narayan's "semantic gap" between specification and
results, i.e., if you actually enforce the specifications will you
really get the effect you seek. Well, if you have a correct compiler you
will get the correct effect. So, the real question is whether you can
express your intuitions well enough in logic. Ed provided a realistic
example but I don't think there is any problem in expressing it
-intuitively- in Alloy or Prolog. Instead of treating it as one giant
constraint, you define intermediate predicates and compose these. This
is analogous to what you do in a programming language such as Perl. You
define simple procedures then assemble these into more complex ones.
Narayan also raised the concern that enforcement of global constraints
is dicey because administrative control is often not centralized, but
rather distributed across many administrators. However, I don't see why
this is related to logic. Wouldn't this arise with any attempt at
automatic reconfiguration that spans multiple administrative domains?
Efficient enforcement of constraints is a genuine concern and the
subject of our current research. But, please note that enforcement is
NOT the only use of a specification. Diagnosis is another very important
use. Since it is read-only it avoids the above "semantic gap" concern.
Network administrators routinely create network diagrams. These can be
regarded as Boolean constraints. But these leave out important parts of
their intended policy such as "for every IPSec tunnel originating at a
router, there is a static route that directs traffic for the remote
destination into the tunnel". I don't see any simple way of graphically
specifying such constraints. Therefore, can't we provide a few primitive
constraints along with FOL operators for composing these, and expect
administrators to supply the missing pieces of their intended policy? --
Sanjai
[EMAIL PROTECTED] wrote:
Quoting Sanjai Narain <[EMAIL PROTECTED]>:
Logic-based languages are great for expressing complex constraints
arising in system administration. However, it is also considered
axiomatic that system administrators will never use such languages.
The reason given is that they require too much mathematical training.
I don't think this is the only reason - eventually, there will need to
be some formal education associated with system administration, the
same way you wouldn't let a guy who "kinda fixes his car sometimes"
service the engines on a 747. But what that education should consist
of is still up for grabs I think? (This is a deep hole on its own).
In my opinion, predicate logic is very, very dense. Different
orderings of predicates can have subtly different meanings, leading to
(disastrously?) different solutions from segments of code which differ
very little.
When I was working on examples for cfgw like "my redundancy isnt
invalidated by mapping multiple redundant virtual instances to a
single physical node" and "each and every client is pointing at a
server which exists, and which supplies the service it is requesting"
I found it relatively difficult to specify these correctly, because of
the difficulty of keeping track of exactly which quantifiers were in
play, and of rephrasing what I wanted to say in terms of
quantification. (e.g. for all p a physical node, and any v a virtual
node, where v is mapped to p, then for any w a virtual node, where w
is not v, then if s is a service, and s needs redundancy, and v
provides s, and w provides s, then w is not mapped to p... there are
probably errors in this example, and I'm sure it can be coded more
efficiently, my point is just to illustrate that for casual use, this
is very dense, and small changes can have far reaching implications).
I think that training could help, but I think that widespread use of
predicate logic is a long way off. In an environment in which safety
is at a highly desirable, I think it is a mistake to think a more
powerful tool is preferrable. In general, its more likely people will
be buying into safety rails than high performance engines in the future.
I would like to challenge this view. What is so hard about logic?
Everyone knows Boolean constraints. First-order logic is simply
Boolean logic + quantifiers. This is adequate for specifying a very
large class of constraints. If system administrators can handle
complexities of procedural languages like Perl, then surely a
declarative language like FOL should be a breeze, shouldn't it? In
particular, I think we should stop trying hard to sweep FOL under the
rug of GUIs. Even if we could create a GUI in which one could express
all of FOL, it would be so cumbersome that it would be much easier to
use text. What do you think? -- Sanjai
I think the attraction of GUIs (I don't know if its just GUIs; I see
no reason why a CLI with options couldn't provide the same benefits)
is that they can provide (perhaps using first-order logic) a set of
things for administrators to do which are tested and safe, which can
then be merely activated.
I don't think the objective is to replicate the functionality provided
by first order logic. I think that really, formally specifying the
exact predicates in operation on the network is something people want
to do now, because they have no idea what predicates operate on their
network, and no way to try it. I think this is the same as if we had
terrible opaque tools and no compilers or assemblers: people would say
now that they want to write their own. We have compilers, and what
people want is for someone else to write the tools, because formally
specifying the exact process by which to accomplish each task is hard
and time consuming. The same will hold (perhaps even more so) for
logical assertions like these. People simply want a "good enough"
option to select. I think the objective is to pick the 10-50 things
you were most likely to use formal specification for, and then provide
those as options.
Ed
_______________________________________________
lssconf-discuss mailing list
lssconf-discuss@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/lssconf-discuss
--
Sanjai Narain, Ph.D.
Senior Research Scientist
Information Assurance and Security Department
Telcordia Technologies, Inc.
1 Telcordia Drive, Room 1N-375
Piscataway, NJ 08854
732 699 2806 (T)
908 337 3636 (M)
[EMAIL PROTECTED]
_______________________________________________
lssconf-discuss mailing list
lssconf-discuss@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/lssconf-discuss
